################################################################################
                            About of this File
################################################################################

This directory contains several verification benchmarks generated using the Averest system. Averest is a software library for the simulation, verification and synthesis of synchronous reactive programs written in the Quartz synchronous language. It has been implemented in F# with .NET 10, enabling it to run on a variety of platforms, including MacOS with ARM and x64 processors, as well as Linux and Windows.


################################################################################
                        Resource Requirements
################################################################################

To run these proof scripts, you need a computer with an installation of .NET 10, which you can download from https://dotnet.microsoft.com/ for the aforementioned platforms. Once installed, you just need to call 'dotnet' from the command line. If you want, you can work through the proof scripts in interactive F# sessions.

Averest is available as a NuGet package from https://www.nuget.org/packages/Averest. Further information can be found at http://averest.org/. In particular, documentation for the proof rules can be found at http://averest.org/averestlibdoc/reference/index.html. 

For your convenience, this directory contains all the libraries required to run the proof scripts: 
   
    ./lib:
        Averest.dll
        Averest.xml
        FsLexYacc.Runtime.dll
        FsLexYacc.Runtime.xml
        Microsoft.Z3.dll
        Microsoft.Z3.xml
    
    ./runtimes/
        linux-arm64/native/libz3.so
        linux-x64/native/libz3.so
        osx-arm64/native/libz3.dylib
        osx-x64/native/libz3.dylib
        win-arm64/native/libz3.dll
        win-x64/native/libz3.dll

Averest.dll and FsLexYacc.Runtime.dll are platform-independent, whereas Microsoft's Z3 SMT prover has been compiled natively for the aforementioned platforms: Windows, MacOS and Linux with arm64 and x64 processors, respectively. 


################################################################################
                        Further Content of this File
################################################################################

The directory 'doc' contains the 'Quartz.pdf' tutorial about the synchronous language Quartz, which is used to describe systems for verification. It also contains the 'ref-prover.pdf' cheat sheet, which lists the proof rules implemented in Averest's interactive theorem prover.

The proof scripts can be found in directory 'src' which contains the following verification examples: 

    - AcptConditions/
        Acpt1.fsx*
        Acpt2.fsx*
        Acpt3.fsx*
        TransitionSystems/
    - Arithmetic/
        AddByIteratedInc.fsx*
        DivisionByIteratedSub.fsx*
        DivisionNonperform.fsx*
        DivisionNonrestoring.fsx*
        DivisionRestoring.fsx*
        Exponential.fsx
        ExtEuclid.fsx*
        MultByIteratedAdd.fsx*
        RussMult.fsx*
        SquareRoot1.fsx*
        SquareRoot2.fsx*
        SquareRoot3.fsx*
        SquareRoot4.fsx*
    - Circuits:
        RS-Gated-NOR-FlipFlop.fsx
        RS-NAND-FlipFlop.fsx
        RS-NOR-FlipFlop.fsx
        SinglePulser.fsx
    - DistribSys:
        DijkstraTokenRing.fsx*
        Peterson.fsx*
        WiseMen.fsx*
        TransitionSystems/
    - Interleaving:
        Fairness.fsx*
        Nondet1.fsx*
        Nondet2.fsx*
        Nondet3.fsx*
        PingPong.fsx*
        TransitionSystems/
    - IslandTraffic.fsx
    - IslandTraffic:
        IslandTraffic.fsx*
        IslandTraffic.qrz*
        IslandTraffic.smv*
        TransitionSystems/
    - MinePump:
        doc/
        MinePump.fsx*
        MinePump.smv*
        TransitionSystems/
    - Misc:
        BenA12.fsx*
        DivMod.fsx
        IncorrectGenTac.fsx*
    - TemporalLogicThms.fsx
    - Termination:
        Termination0.fsx*
        Termination1.fsx*
        Termination2.fsx*
        Termination3.fsx*
        Termination4.fsx*
        Termination5.fsx*
        Termination6.fsx*
        Termination7.fsx*
        Termination8.fsx*
        Termination9.fsx*
        Chameleons.fsx
        CoffeeCanGries.fsx*
        Ducci.pdf
        Ducci.tex
        DucciBool4.fsx
        DucciBool9.fsx
        DucciInt3.fsx
        DucciInt4.fsx
        DucciNat3.fsx
        DucciNat4.fsx
        Engel3.fsx
        Engel4.fsx
        Engel4.pdf
        Engel4.tex
        McCarthy91.fsx*
        Pentagon1.fsx*
        Pentagon2.fsx*
        SwapSort.fsx
        TransitionSystems/
    - VendingMachine/
        VendingMachine.fsx
    - WellfareCrook.fsx



################################################################################
                        How to Check the Proofs
################################################################################

The above-listed F# scripts (fsx-files) typically begin by loading a Quartz program into the proof context. This means that subsequent proof goals and proofs refer to this module. The Quartz program is then translated into an equation system, the equations of which can be displayed using the PrintNowEquations and PrintNxtEquations functions. The declarations are used in the ParseSpecExprFromString and ParseExprFromString functions, which parse specifications and expressions from strings. After loading the Quartz program into the proof context, the file lists the proof goals and their associated proofs, i.e. rule applications. There are two ways to run these proof scripts, explained below. 

--------------------------------------------------------------------------------
                    Run all Proof Scripts Automatically
--------------------------------------------------------------------------------

In order to run all F# scripts automatically, you must select one of the following commands, depending on your platform, and copy it into a terminal window on your computer. 

    - MacOS with arm64:   dotnet fsi --define:osxArm64 runScript.fsx                              
    - MacOS with x64:     dotnet fsi --define:osxX64 runScript.fsx                              
    - Linux with x64:     dotnet fsi --define:linuxX64 runScript.fsx                               
    - Windows with x64:   dotnet fsi --define:winX64 runScript.fsx

This call establishes the necessary paths to the libraries for your platform and then invokes the 'src/00-doAll.fsx' file, which serves as the primary F# script responsible for loading all the aforementioned proof scripts. 

Instead of running all scripts one after another, you can also run a single script. To do so, you have to replace the load instruction at the end of 'runScript.fsx' with the script you want to run, or you can write your own script by copying the path settings for your platform from 'runScript.fsx' and the initial part to open modules and define some functions in 'src/00-doAll.fsx' as shown by script src/il.fsx' which runs the proof of the Island Traffic benchmark. 


--------------------------------------------------------------------------------
                    Using Proof Scripts Interactively
--------------------------------------------------------------------------------

The strength of Averest is the ability to develop proofs interactively which generally aims at reducing proof goals to simpler ones that can be solved by automated decision procedures. Running the proofs as explained above is good for regression tests, but that does not show how users really work with the Averest prover.

If you would like to see how proof goals are reduced interactively by applying proof rules, take a look at the 'src/00-useProofTactics.fs' file. First, start an interactive F# session using the 'dotnet fsi' command line (including any necessary path and library calls). 

In the F# interactive session, a Quartz program must first be loaded into the proof context. Then, you can use function SetNewGoal to determine a new proof goal. For this, you must provide a name for the goal, as well as any assumptions and the conclusion to be proved. After this, you can apply a proof rule f simply by applying the f() function, i.e. by typing f() in the F# interactive session. The current proof goal is then broken down into subgoals, which are printed. You can then apply the next rule until no subgoals remain. At this point, the proof goal becomes a theorem and is stored under the given name in the proof context, ready for use in further proofs. 

The 'ProveThm name goal rule' function calls found in the fsx-files is just an abbreviation for setting a new proof goal with the specified name and goal, and then applying the given proof rule to it. Therefore, you can replace them with a corresponding 'SetNewGoal' call, allowing you to apply the proof rules step by step. rules step by step. 


################################################################################
                                end of file
################################################################################
