From d89f14ee146bf069a32e9e1802c7cbbbe96bd5d4 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 13 Jun 2013 12:45:47 +0200 Subject: [PATCH] model-checker : update bugged1 and bugged2 tesh (different compilation flags) --- examples/msg/mc/bugged1.tesh | 13 ++++++++++--- examples/msg/mc/bugged2.tesh | 2 +- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/examples/msg/mc/bugged1.tesh b/examples/msg/mc/bugged1.tesh index 7806f8f1a5..78c1f5ef81 100644 --- a/examples/msg/mc/bugged1.tesh +++ b/examples/msg/mc/bugged1.tesh @@ -10,6 +10,13 @@ $ ${bindir:=.}/bugged1 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)% > [ 0.000000] (1:server@HostA) OK > [ 0.000000] (4:client@HostD) Sent! > [ 0.000000] (2:client@HostB) Sent! +> [ 0.000000] (3:client@HostC) Sent! +> [ 0.000000] (2:client@HostB) Sent! +> [ 0.000000] (3:client@HostC) Sent! +> [ 0.000000] (1:server@HostA) OK +> [ 0.000000] (4:client@HostD) Sent! +> [ 0.000000] (2:client@HostB) Sent! +> [ 0.000000] (3:client@HostC) Sent! > [ 0.000000] (2:client@HostB) Sent! > [ 0.000000] (1:server@HostA) ************************** > [ 0.000000] (1:server@HostA) *** PROPERTY NOT VALID *** @@ -25,6 +32,6 @@ $ ${bindir:=.}/bugged1 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)% > [ 0.000000] (1:server@HostA) [(1)HostA (server)] iRecv (dst=(1)HostA (server), buff=(verbose only), size=(verbose only)) > [ 0.000000] (1:server@HostA) [(3)HostC (client)] iSend (src=(3)HostC (client), buff=(verbose only), size=(verbose only)) > [ 0.000000] (1:server@HostA) [(1)HostA (server)] Wait (comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)]) -> [ 0.000000] (1:server@HostA) Expanded states = 17 -> [ 0.000000] (1:server@HostA) Visited states = 32 -> [ 0.000000] (1:server@HostA) Executed transitions = 30 +> [ 0.000000] (1:server@HostA) Expanded states = 22 +> [ 0.000000] (1:server@HostA) Visited states = 56 +> [ 0.000000] (1:server@HostA) Executed transitions = 52 diff --git a/examples/msg/mc/bugged2.tesh b/examples/msg/mc/bugged2.tesh index e6cb1bed4d..bbfd7ac102 100644 --- a/examples/msg/mc/bugged2.tesh +++ b/examples/msg/mc/bugged2.tesh @@ -700,7 +700,7 @@ $ ${bindir:=.}/bugged2 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)% > [ 0.000000] (3:client@HostC) Send 2! > [ 0.000000] (2:client@HostB) Send 1! > [ 0.000000] (1:server@HostA) Received 2 -+ [ 0.000000] (1:server@HostA) Received 1 +> [ 0.000000] (1:server@HostA) Received 1 > [ 0.000000] (1:server@HostA) OK > [ 0.000000] (1:server@HostA) Received 2 > [ 0.000000] (1:server@HostA) Received 1 -- 2.20.1