diff --git a/salut/test/ring-orientation/verify.lus b/salut/test/ring-orientation/verify.lus index 48685d9faa5602a4c95ba238f27a39da083c67eb..9e5aa02f98a0c3d5afa064132e6ceb241feaecd0 100644 --- a/salut/test/ring-orientation/verify.lus +++ b/salut/test/ring-orientation/verify.lus @@ -24,5 +24,5 @@ let worst_case_is_tigth = (round_nb >= worst_case-1) => legitimate; ok = -- 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; \ No newline at end of file diff --git a/salut/test/run-kind2.sh b/salut/test/run-kind2.sh index 61397497f10af2406222825b4552747a887d11d5..89db6cbff6208b285ea1b50ae81d14e98b913cab 100755 --- a/salut/test/run-kind2.sh +++ b/salut/test/run-kind2.sh @@ -15,7 +15,7 @@ where: - n is the size of the topology [1] - 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) - - 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) 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 [3] cf kind2 documentation " +kind2 --version || { echo "kind2 is not installed. try: opam install kind2" ; exit 2; } + #### Dealing with CL arguments # at least 2 arguments are required if [[ $# < 2 ]]