From 82a050fd6b958f8d88bcbb40eb9f5f7f5f936737 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 26 Jun 2014 17:49:52 +0200 Subject: [PATCH 1/1] model-checker : update tesh --- examples/smpi/mc/non_deterministic.tesh | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/examples/smpi/mc/non_deterministic.tesh b/examples/smpi/mc/non_deterministic.tesh index 300dace705..e5120db9f4 100644 --- a/examples/smpi/mc/non_deterministic.tesh +++ b/examples/smpi/mc/non_deterministic.tesh @@ -14,27 +14,34 @@ $ ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_non_determini > [0.000000] [mc_global/INFO] Check communication determinism > [0.000000] [mc_global/INFO] Get debug information ... > [0.000000] [mc_global/INFO] Get debug information done ! +> [0.000000] [mc_comm_determinism/INFO] The communications pattern of the process 1 is different! > [0.000000] [mc_comm_determinism/INFO] **************************************************** > [0.000000] [mc_comm_determinism/INFO] ***** Non-deterministic communications pattern ***** > [0.000000] [mc_comm_determinism/INFO] **************************************************** -> [0.000000] [mc_comm_determinism/INFO] Initial communications pattern: +> [0.000000] [mc_comm_determinism/INFO] ** Initial communications pattern (per process): ** +> [0.000000] [mc_comm_determinism/INFO] Communications from the process 1: > [0.000000] [mc_comm_determinism/INFO] [(1) c-1.me <- (2) c-2.me] iRecv -> [0.000000] [mc_comm_determinism/INFO] [(2) c-2.me -> (1) c-1.me] iSend > [0.000000] [mc_comm_determinism/INFO] [(1) c-1.me -> (2) c-2.me] iSend -> [0.000000] [mc_comm_determinism/INFO] [(2) c-2.me <- (1) c-1.me] iRecv > [0.000000] [mc_comm_determinism/INFO] [(1) c-1.me <- (3) c-3.me] iRecv -> [0.000000] [mc_comm_determinism/INFO] [(3) c-3.me -> (1) c-1.me] iSend > [0.000000] [mc_comm_determinism/INFO] [(1) c-1.me -> (3) c-3.me] iSend +> [0.000000] [mc_comm_determinism/INFO] Communications from the process 2: +> [0.000000] [mc_comm_determinism/INFO] [(2) c-2.me -> (1) c-1.me] iSend +> [0.000000] [mc_comm_determinism/INFO] [(2) c-2.me <- (1) c-1.me] iRecv +> [0.000000] [mc_comm_determinism/INFO] Communications from the process 3: +> [0.000000] [mc_comm_determinism/INFO] [(3) c-3.me -> (1) c-1.me] iSend > [0.000000] [mc_comm_determinism/INFO] [(3) c-3.me <- (1) c-1.me] iRecv -> [0.000000] [mc_comm_determinism/INFO] Communications pattern counter-example: +> [0.000000] [mc_comm_determinism/INFO] ** Communications pattern counter-example (per process): ** +> [0.000000] [mc_comm_determinism/INFO] Communications from the process 1: > [0.000000] [mc_comm_determinism/INFO] [(1) c-1.me <- (3) c-3.me] iRecv -> [0.000000] [mc_comm_determinism/INFO] [(3) c-3.me -> (1) c-1.me] iSend > [0.000000] [mc_comm_determinism/INFO] [(1) c-1.me -> (3) c-3.me] iSend -> [0.000000] [mc_comm_determinism/INFO] [(2) c-2.me -> (1) c-1.me] iSend -> [0.000000] [mc_comm_determinism/INFO] [(3) c-3.me <- (1) c-1.me] iRecv > [0.000000] [mc_comm_determinism/INFO] [(1) c-1.me <- (2) c-2.me] iRecv > [0.000000] [mc_comm_determinism/INFO] [(1) c-1.me -> (2) c-2.me] iSend +> [0.000000] [mc_comm_determinism/INFO] Communications from the process 2: +> [0.000000] [mc_comm_determinism/INFO] [(2) c-2.me -> (1) c-1.me] iSend > [0.000000] [mc_comm_determinism/INFO] [(2) c-2.me <- (1) c-1.me] iRecv +> [0.000000] [mc_comm_determinism/INFO] Communications from the process 3: +> [0.000000] [mc_comm_determinism/INFO] [(3) c-3.me -> (1) c-1.me] iSend +> [0.000000] [mc_comm_determinism/INFO] [(3) c-3.me <- (1) c-1.me] iRecv > [0.000000] [mc_global/INFO] Expanded states = 16037 > [0.000000] [mc_global/INFO] Visited states = 80801 > [0.000000] [mc_global/INFO] Executed transitions = 76048 -- 2.20.1