From d994b72850516592ec42dd81931a9f0bd4e01a6e Mon Sep 17 00:00:00 2001
From: Guillaume Emile <emile.guillaume@etu.univ-grenoble-alpes.fr>
Date: Thu, 23 Jun 2022 16:24:45 +0200
Subject: [PATCH] test: fix expected property
---
test/unison/unison.ml | 2 +-
test/unison/unison_oracle.lus | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/test/unison/unison.ml b/test/unison/unison.ml
index 87a840a5..cdeed961 100644
--- a/test/unison/unison.ml
+++ b/test/unison/unison.ml
@@ -5,7 +5,7 @@ open Algo
(* let m=10 (* max 2 (1+2*diameter ()) *) *)
let diameter = Algo.diameter ()
-let m = max 2 (1+2*diameter)
+let m = max 2 (2*diameter-1)
let (init_state: int -> string -> 'v) =
fun _ _ ->
diff --git a/test/unison/unison_oracle.lus b/test/unison/unison_oracle.lus
index 861e7456..e1950889 100644
--- a/test/unison/unison_oracle.lus
+++ b/test/unison/unison_oracle.lus
@@ -9,7 +9,7 @@ var
let
nb_step = 1 -> pre(nb_step) + 1 ;
All_Acti = all_true<<an,pn>>(Acti);
- res = ((max_clock>= (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
--
GitLab