Skip to content
Snippets Groups Projects
Commit 1624f606 authored by erwan's avatar erwan
Browse files

test: exit in error if kind2 is not installed

parent 0a2790fc
No related branches found
No related tags found
No related merge requests found
...@@ -24,5 +24,5 @@ let ...@@ -24,5 +24,5 @@ let
worst_case_is_tigth = (round_nb >= worst_case-1) => legitimate; worst_case_is_tigth = (round_nb >= worst_case-1) => legitimate;
ok = ok =
-- closure is wrong because legitimate needs to be more specific (cf state.lus) -- closure is wrong because legitimate needs to be more specific (cf state.lus)
converge_worst_case ; -- closure and; closure and converge_worst_case ; -- closure and;
tel; tel;
\ No newline at end of file
...@@ -15,7 +15,7 @@ where: ...@@ -15,7 +15,7 @@ where:
- n is the size of the topology [1] - n is the size of the topology [1]
- property is one of the verify node variable (in verify.lus) (ok by default) - property is one of the verify node variable (in verify.lus) (ok by default)
- daemon is in {synchronous,distributed,central,locally_central} (distributed by default) - daemon is in {synchronous,distributed,central,locally_central} (distributed by default)
- int is in {int, int8, uint8, int16, uint16, ..., uinit64} [2] (int by default) - int is in {int, int8, uint8, int16, uint16, ..., uinit64} [2] (int8+ by default)
- solver is in {Z3, Bitwuzla, cvc5, MathSAT, Yices, Yices2} [3] (Bitwuzla by default) - solver is in {Z3, Bitwuzla, cvc5, MathSAT, Yices, Yices2} [3] (Bitwuzla by default)
example of use (that are equivalent because of the default values): example of use (that are equivalent because of the default values):
...@@ -40,6 +40,8 @@ nb: '$0 file_name_unknown_to_gg 5' works if 'file_name_unknown_to_gg5.dot' exist ...@@ -40,6 +40,8 @@ nb: '$0 file_name_unknown_to_gg 5' works if 'file_name_unknown_to_gg5.dot' exist
[3] cf kind2 documentation [3] cf kind2 documentation
" "
kind2 --version || { echo "kind2 is not installed. try: opam install kind2" ; exit 2; }
#### Dealing with CL arguments #### Dealing with CL arguments
# at least 2 arguments are required # at least 2 arguments are required
if [[ $# < 2 ]] if [[ $# < 2 ]]
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment