diff --git a/dune-project b/dune-project index 929c696e5619afde4d3ce417325e0a4d5c0acd1a..e66023f9222a0775c89e4c950b3dc6d799b9671f 100644 --- a/dune-project +++ b/dune-project @@ -1 +1,4 @@ (lang dune 2.0) +(authors "Erwan Jahier") + +(maintainers "Erwan Jahier") diff --git a/test/unison/unison_oracle.lus b/test/unison/unison_oracle.lus index d6f04be6eb4329cdf63159f9315c4373045b7804..23a84b9774f51bc9710de29242bb1a8197237a2c 100644 --- a/test/unison/unison_oracle.lus +++ b/test/unison/unison_oracle.lus @@ -10,7 +10,7 @@ var let nb_step = 1 -> pre(nb_step) + 1 ; All_Acti = all_true<<an,pn>>(Acti); - res = (((2*diameter-1)>= (2*diameter-1)) and is_connected) + res = (((2*diameter-1) >= (2*diameter-1)) and is_connected) => (nb_step>=(3*diameter-2)) => All_Acti ; -- Theorem 4.11 page 40 tel