Skip to content

Commit

Permalink
session files
Browse files Browse the repository at this point in the history
  • Loading branch information
jspdium committed Apr 10, 2024
2 parents e95b6e8 + df89a2e commit 760ec8f
Show file tree
Hide file tree
Showing 12 changed files with 246 additions and 72 deletions.
80 changes: 80 additions & 0 deletions .github/workflows/set-up-environment.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
name: replay-why3-proofs
run-name: ${{ github.actor }} setting up environment
on: [push]
env:
CVC4_URL: "https://github.com/CVC4/CVC4-archived/releases/download/1.8/cvc4-1.8-x86_64-linux-opt"
CVC5_URL: "https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.3/cvc5-Linux"
Z3_URL: "https://github.com/Z3Prover/z3/releases/download/z3-4.11.2/z3-4.11.2-x64-glibc-2.31.zip"
jobs:
install-and-test:
runs-on: ubuntu-latest
steps:
- name: Check out repository code
uses: actions/checkout@v3
- name: Use OCaml
uses: ocaml/setup-ocaml@v2
with:
ocaml-compiler: 4.13.x
- name: install tools with opam
run: |
opam update
opam install why3.1.6.0
opam install alt-ergo.2.4.2
opam install eprover.2.6
# it's possible to install z3 as follows
# opam install z3.4.11.2
- name: download z3, cvc4, and cvc5
run: |
mkdir downloads
cd downloads
wget $CVC4_URL
chmod +x ${CVC4_URL##*/}
mv ${CVC4_URL##*/} /usr/local/bin/cvc4
# echo "deb http://cvc4.cs.nyu.edu/debian/ unstable/" | sudo tee -a /etc/apt/sources.list
# echo "deb-src http://cvc4.cs.nyu.edu/debian/ unstable/" | sudo tee -a /etc/apt/sources.list
# sudo apt-get update
# sudo apt-get install cvc4 --force-yes
wget $CVC5_URL
chmod +x ${CVC5_URL##*/}
mv ${CVC5_URL##*/} /usr/local/bin/cvc5
# also possible to use opam to install z3, but the compilation is very slow
wget $Z3_URL
z3folder=${Z3_URL##*/}
unzip $z3folder
mv ${z3folder%.*}/bin/z3 /usr/local/bin
- name: test installation
run: |
eval $(opam env)
echo "which why3"
which why3
echo "why3 version"
why3 --version
echo "which alt-ergo"
which alt-ergo
echo "alt-ergo --version"
alt-ergo --version
echo "which z3"
which z3
echo "z3 --version"
z3 --version
echo "which cvc4"
which cvc4
echo "cvc4 --version"
cvc4 --version
echo "which cvc5"
which cvc5
echo "cvc5 --version"
cvc5 --version
- name: replay proofs
run: |
echo "eval $(opam env)"
eval $(opam env)
echo "why3 config detect"
why3 config detect
echo "why3 config list-provers"
why3 config list-provers
echo "cd $GITHUB_WORKSPACE"
cd $GITHUB_WORKSPACE
echo "# Replay Status" > $GITHUB_STEP_SUMMARY
echo "./test.sh"
./test.sh
16 changes: 11 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,11 +1,17 @@
# Why3-do

[![Why3 proof replay][workflow-badge]][workflow]

[workflow]: https://github.com/haslab/why3do/actions/workflows/set-up-environment.yml
[workflow-badge]: https://img.shields.io/github/actions/workflow/status/haslab/why3do/set-up-environment.yml?label=Proof%20Replay&logo=github

A WhyML library for reasoning about state machine specifications and distributed systems

## Library Modules

* [stateMachineModels](stateMachineModels): theories for
inductive invariants and refinement mappings of state machine
specifications
specifications
* [networkModels](networkModels): theories for reasoning about
distributed systems with different network semantics

Expand All @@ -20,10 +26,10 @@ A WhyML library for reasoning about state machine specifications and distributed
* [twoPhase](examples/twoPhase): Two-phase handshake protocol, refined
from abstract specification
* [counter](examples/counter): Concurrent counter using a lock,
by refinement from abstract specification
by refinement from abstract specification
* [mutualExclusionConcurrent](examples/mutualExclusionConcurrent):
Mutual exclusion algorithms for concurrent processes, refined from
an abstract specification
an abstract specification
* [waitFreeRegister](examples/waitFreeRegister): Wait-free
implementation of a shared register using non-atomic registers
* [leaderElection](examples/leaderElection/): Chang-Roberts leader
Expand All @@ -38,11 +44,11 @@ A WhyML library for reasoning about state machine specifications and distributed

## Example commands

* `why3 ide examples/leaderElection/ChangRoberts.mlw -L examples/leaderElection -L stateMachineModels`: (executed in the top-level folder) launches the Why3 IDE with file `ChangRoberts.mlw`
* `why3 ide examples/leaderElection/ChangRoberts.mlw -L examples/leaderElection -L stateMachineModels`: (executed in the top-level folder) launches the Why3 IDE with file `ChangRoberts.mlw`
* `why3 replay examples/leaderElection/ChangRoberts -L
examples/leaderElection -L stateMachineModels`: replays the proof
session of the same example (assuming all the required SMT solvers are present in the local setup)
* `why3 replay --smoke-detector=top examples/leaderElection/ChangRoberts -L
examples/leaderElection -L stateMachineModels`: runs inconsistency
detection on the proof session of the same example
detection on the proof session of the same example

2 changes: 1 addition & 1 deletion examples/distributedLockNetwork/LDTDupl/why3session.xml
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@
<proof prover="7" timelimit="1"><result status="valid" time="0.77" steps="6255"/></proof>
</goal>
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.5" expl="postcondition" proved="true">
<proof prover="7" timelimit="5"><result status="valid" time="2.68" steps="42422"/></proof>
<proof prover="5" timelimit="10" memlimit="1000"><result status="valid" time="1.22" steps="158463"/></proof>
</goal>
<goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.6" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="1.15" steps="84540"/></proof>
Expand Down
2 changes: 1 addition & 1 deletion examples/leaderElection/ChangRoberts/why3session.xml
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@
<goal name="act&#39;vc.0.9.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="act&#39;vc.0.9.0.0" expl="postcondition" proved="true">
<proof prover="3" memlimit="2000"><result status="valid" time="1.51" steps="125186"/></proof>
<proof prover="3" timelimit="20"><result status="valid" time="13.78" steps="904149"/></proof>
</goal>
</transf>
</goal>
Expand Down
Loading

0 comments on commit 760ec8f

Please sign in to comment.