model-checker : revalidate tesh

diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh
index 94b5a1d..5f72c22 100644 (file)
--- a/examples/msg/mc/bugged1_liveness.tesh
+++ b/examples/msg/mc/bugged1_liveness.tesh
@@ -15,7 +15,7 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcd
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
 > [  0.000000] (3:client@Fafard) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [  0.000000] (0:@) Pair 21 already reached (equal to pair 9) !
+> [  0.000000] (0:@) Pair 22 already reached (equal to pair 10) !
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
@@ -40,7 +40,8 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcd
 > [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
 > [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [  0.000000] (0:@) Expanded pairs = 21
-> [  0.000000] (0:@) Visited pairs = 21
+> [  0.000000] (0:@) Expanded pairs = 22
+> [  0.000000] (0:@) Visited pairs = 20
 > [  0.000000] (0:@) Executed transitions = 20
-> [  0.000000] (0:@) Counter-example depth : 20
+> [  0.000000] (0:@) Counter-example depth : 21
+

diff --git a/examples/msg/mc/bugged1_liveness_sparse.tesh b/examples/msg/mc/bugged1_liveness_sparse.tesh
index f5100d6..bc934d9 100644 (file)
--- a/examples/msg/mc/bugged1_liveness_sparse.tesh
+++ b/examples/msg/mc/bugged1_liveness_sparse.tesh
@@ -16,7 +16,7 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcd
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
 > [  0.000000] (3:client@Fafard) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [  0.000000] (0:@) Pair 21 already reached (equal to pair 9) !
+> [  0.000000] (0:@) Pair 22 already reached (equal to pair 10) !
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
@@ -41,7 +41,7 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcd
 > [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
 > [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [  0.000000] (0:@) Expanded pairs = 21
-> [  0.000000] (0:@) Visited pairs = 21
+> [  0.000000] (0:@) Expanded pairs = 22
+> [  0.000000] (0:@) Visited pairs = 20
 > [  0.000000] (0:@) Executed transitions = 20
-> [  0.000000] (0:@) Counter-example depth : 20
+> [  0.000000] (0:@) Counter-example depth : 21

diff --git a/examples/msg/mc/bugged1_liveness_visited.tesh b/examples/msg/mc/bugged1_liveness_visited.tesh
index 30ed49f..d05858a 100644 (file)
--- a/examples/msg/mc/bugged1_liveness_visited.tesh
+++ b/examples/msg/mc/bugged1_liveness_visited.tesh
@@ -73,7 +73,7 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcd
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [  0.000000] (0:@) Pair 57 already reached (equal to pair 45) !
+> [  0.000000] (0:@) Pair 58 already reached (equal to pair 46) !
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
@@ -128,7 +128,8 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcd
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
 > [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
 > [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:@) Expanded pairs = 57
-> [  0.000000] (0:@) Visited pairs = 208
+> [  0.000000] (0:@) Expanded pairs = 58
+> [  0.000000] (0:@) Visited pairs = 201
 > [  0.000000] (0:@) Executed transitions = 207
-> [  0.000000] (0:@) Counter-example depth : 50
+> [  0.000000] (0:@) Counter-example depth : 51
+

diff --git a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh
index bd9981d..9e987ea 100644 (file)
--- a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh
+++ b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh
@@ -74,7 +74,7 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcd
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
 > [  0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [  0.000000] (0:@) Pair 57 already reached (equal to pair 45) !
+> [  0.000000] (0:@) Pair 58 already reached (equal to pair 46) !
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
@@ -129,7 +129,7 @@ $ ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcd
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
 > [  0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
 > [  0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:@) Expanded pairs = 57
-> [  0.000000] (0:@) Visited pairs = 208
+> [  0.000000] (0:@) Expanded pairs = 58
+> [  0.000000] (0:@) Visited pairs = 201
 > [  0.000000] (0:@) Executed transitions = 207
-> [  0.000000] (0:@) Counter-example depth : 50
+> [  0.000000] (0:@) Counter-example depth : 51