> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) Counter-example execution trace:
-> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
-> [ 0.000000] (0:maestro@) 2: iSend(mbox=0)
-> [ 0.000000] (0:maestro@) 1: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
-> [ 0.000000] (0:maestro@) 2: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) 4: iSend(mbox=0)
-> [ 0.000000] (0:maestro@) 1: WaitComm(from 4 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
-> [ 0.000000] (0:maestro@) 3: iSend(mbox=0)
-> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 2 in Isend ==> simcall: iSend(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 2 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 2 in Wait ==> simcall: WaitComm(from 2 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 4 in Isend ==> simcall: iSend(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 4 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;2;1;1;2;4;1;1;3;1'
> [ 0.000000] (0:maestro@) DFS exploration ended. 19 unique states visited; 2 backtracks (12 transition replays, 33 states visited overall)
> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
> [0.000000] [mc_explo/INFO] **************************
> [0.000000] [mc_explo/INFO] Counter-example execution trace:
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;3;3;1'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 98 unique states visited; 21 backtracks (153 transition replays, 272 states visited overall)
> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
> [0.000000] [mc_explo/INFO] **************************
> [0.000000] [mc_explo/INFO] Counter-example execution trace:
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 2: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 2 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;3;3;2;1'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 83 unique states visited; 12 backtracks (65 transition replays, 160 states visited overall)
> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
> [0.000000] [mc_explo/INFO] **************************
> [0.000000] [mc_explo/INFO] Counter-example execution trace:
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;3;1'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 44 unique states visited; 3 backtracks (11 transition replays, 58 states visited overall)
> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
> [0.000000] [mc_explo/INFO] **************************
> [0.000000] [mc_explo/INFO] Counter-example execution trace:
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 2: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 2 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 2 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;2;1'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 24 unique states visited; 8 backtracks (26 transition replays, 58 states visited overall)
> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
> [0.000000] [mc_explo/INFO] **************************
> [0.000000] [mc_explo/INFO] Counter-example execution trace:
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 2: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 2 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 2 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;2;1'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 14 unique states visited; 1 backtracks (1 transition replays, 16 states visited overall)
> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
> [0.000000] [mc_explo/INFO] **************************
> [0.000000] [mc_explo/INFO] Counter-example execution trace:
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 2: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
-> [0.000000] [mc_explo/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 2 in Isend ==> simcall: iSend(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [0.000000] [mc_explo/INFO] Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] Actor 1 in Wait ==> simcall: WaitComm(from 2 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;2;1;3;1;1'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 29 unique states visited; 10 backtracks (26 transition replays, 65 states visited overall)
\ No newline at end of file
> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) Counter-example execution trace:
-> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
-> [ 0.000000] (0:maestro@) 3: iSend(mbox=0)
-> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
-> [ 0.000000] (0:maestro@) 2: iSend(mbox=0)
-> [ 0.000000] (0:maestro@) 1: WaitComm(from 2 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 2 in Isend ==> simcall: iSend(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 2 to 1, mbox=0, no timeout)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;2;1'
> [ 0.000000] (0:maestro@) DFS exploration ended. 15 unique states visited; 2 backtracks (4 transition replays, 21 states visited overall)
> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) Counter-example execution trace:
-> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
-> [ 0.000000] (0:maestro@) 3: iSend(mbox=0)
-> [ 0.000000] (0:maestro@) 2: iSend(mbox=0)
-> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) 3: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
-> [ 0.000000] (0:maestro@) 1: WaitComm(from 2 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 2 in Isend ==> simcall: iSend(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 2 to 1, mbox=0, no timeout)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;2;1;3;1;1'
> [ 0.000000] (0:maestro@) DFS exploration ended. 18 unique states visited; 3 backtracks (1 transition replays, 22 states visited overall)
> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) Counter-example execution trace:
-> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
-> [ 0.000000] (0:maestro@) 3: iSend(mbox=0)
-> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) 3: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [ 0.000000] (0:maestro@) 1: iRecv(mbox=0)
-> [ 0.000000] (0:maestro@) 2: iSend(mbox=0)
-> [ 0.000000] (0:maestro@) 1: WaitComm(from 2 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 3 in Isend ==> simcall: iSend(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 3 in Wait ==> simcall: WaitComm(from 3 to 1, mbox=0, no timeout)
+> [ 0.000000] (0:maestro@) Actor 1 in Irecv ==> simcall: iRecv(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 2 in Isend ==> simcall: iSend(mbox=0)
+> [ 0.000000] (0:maestro@) Actor 1 in Wait ==> simcall: WaitComm(from 2 to 1, mbox=0, no timeout)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;2;1'
> [ 0.000000] (0:maestro@) DFS exploration ended. 14 unique states visited; 1 backtracks (1 transition replays, 16 states visited overall)
\ No newline at end of file
> [0.000000] [ker_engine/INFO] Actor 2 (thread 1@Lilibeth) simcall MUTEX_WAIT(mutex_id:1 owner:3)
> [0.000000] [ker_engine/INFO] Actor 3 (thread 2@Lilibeth) simcall MUTEX_WAIT(mutex_id:0 owner:2)
> [0.000000] [mc_global/INFO] Counter-example execution trace:
-> [0.000000] [mc_global/INFO] 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
-> [0.000000] [mc_global/INFO] 2: MUTEX_WAIT(mutex: 0, owner: 2)
-> [0.000000] [mc_global/INFO] 3: MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
-> [0.000000] [mc_global/INFO] 2: MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
-> [0.000000] [mc_global/INFO] 3: MUTEX_WAIT(mutex: 1, owner: 3)
-> [0.000000] [mc_global/INFO] 3: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_WAIT(mutex: 0, owner: 2)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
+> [0.000000] [mc_global/INFO] Actor 2 in simcall MUTEX_ASYNC_LOCK(mutex: 1, owner: 3)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_WAIT(mutex: 1, owner: 3)
+> [0.000000] [mc_global/INFO] Actor 3 in simcall MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;3;2;3;3'
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 21 unique states visited; 3 backtracks (11 transition replays, 35 states visited overall)
\ No newline at end of file
> [ 0.000000] (maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (maestro@) **************************
> [ 0.000000] (maestro@) Counter-example execution trace:
-> [ 0.000000] (maestro@) 2: BeginObjectAccess(&v)
-> [ 0.000000] (maestro@) 3: BeginObjectAccess(&v)
+> [ 0.000000] (maestro@) Actor 2 in simcall BeginObjectAccess(&v)
+> [ 0.000000] (maestro@) Actor 3 in simcall BeginObjectAccess(&v)
> [ 0.000000] (maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;3'
> [ 0.000000] (maestro@) DFS exploration ended. 7 unique states visited; 1 backtracks (1 transition replays, 9 states visited overall)
std::to_string(linenumber);
}
- std::string get_call_location() const { return filename + "::" + func_call + "::" + std::to_string(linenumber); }
+ std::string get_call_location() const { return filename + ":" + std::to_string(linenumber) + ":" + func_call + "()"; }
};
#endif
std::vector<std::string> Exploration::get_textual_trace()
{
std::vector<std::string> trace;
- for (auto const& transition : get_record_trace())
- trace.push_back(xbt::string_printf("%ld: %s", transition->aid_, transition->to_string().c_str()));
+ for (auto const& transition : get_record_trace()) {
+ auto call_location = transition->get_call_location();
+ if (not call_location.empty())
+ trace.push_back(xbt::string_printf("Actor %ld in %s ==> simcall: %s", transition->aid_, call_location.c_str(),
+ transition->to_string().c_str()));
+ else
+ trace.push_back(xbt::string_printf("Actor %ld in simcall %s", transition->aid_, transition->to_string().c_str()));
+ }
return trace;
}
aid_t aid_ = 0;
- /** The user function call that caused this transition to exist.
- * Format is filename::function::line */
- std::string user_fun_call_ = "";
+ /** The user function call that caused this transition to exist. Format: >>filename:line:function()<< */
+ std::string call_location_ = "";
/* Which transition was executed for this simcall
*
/** Returns something like >>label = "desc", color = c<< to describe the transition in dot format */
virtual std::string dot_string() const;
+ std::string get_call_location() { return call_location_; }
+
/* Moves the application toward a path that was already explored, but don't change the current transition */
void replay(RemoteApp& app) const;
: Transition(Type::COMM_WAIT, issuer, times_considered)
{
xbt_assert(stream >> timeout_ >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_ >>
- user_fun_call_);
+ call_location_);
XBT_DEBUG("CommWaitTransition %s comm:%u, sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR
" size:%zu",
(timeout_ ? "timeout" : "no-timeout"), comm_, sender_, receiver_, mbox_, sbuff_, rbuff_, size_);
CommTestTransition::CommTestTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_TEST, issuer, times_considered)
{
- xbt_assert(stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_ >> user_fun_call_);
+ xbt_assert(stream >> comm_ >> sender_ >> receiver_ >> mbox_ >> sbuff_ >> rbuff_ >> size_ >> call_location_);
XBT_DEBUG("CommTestTransition comm:%u, sender:%ld receiver:%ld mbox:%u sbuff:%" PRIxPTR " rbuff:%" PRIxPTR
" size:%zu",
comm_, sender_, receiver_, mbox_, sbuff_, rbuff_, size_);
CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_ASYNC_RECV, issuer, times_considered)
{
- xbt_assert(stream >> comm_ >> mbox_ >> rbuff_ >> tag_ >> user_fun_call_);
+ xbt_assert(stream >> comm_ >> mbox_ >> rbuff_ >> tag_ >> call_location_);
}
std::string CommRecvTransition::to_string(bool verbose) const
{
CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, std::stringstream& stream)
: Transition(Type::COMM_ASYNC_SEND, issuer, times_considered)
{
- xbt_assert(stream >> comm_ >> mbox_ >> sbuff_ >> size_ >> tag_ >> user_fun_call_);
+ xbt_assert(stream >> comm_ >> mbox_ >> sbuff_ >> size_ >> tag_ >> call_location_);
XBT_DEBUG("SendTransition comm:%u mbox:%u sbuff:%" PRIxPTR " size:%zu", comm_, mbox_, sbuff_, size_);
}
std::string CommSendTransition::to_string(bool verbose = false) const
void LocationAction::kernel(simgrid::xbt::ReplayAction&)
{
const LocationParser& args = get_args();
- smpi_trace_set_call_location(args.filename.c_str(), args.line, "");
+ smpi_trace_set_call_location(args.filename.c_str(), args.line, "replay_action");
}
void TestAction::kernel(simgrid::xbt::ReplayAction&)
> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) Counter-example execution trace:
-> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3)
-> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4)
+> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3)
+> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (19 transition replays, 68 states visited overall)
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) From signal: Aborted
> [ 0.000000] (0:maestro@) Counter-example execution trace:
-> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3)
-> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4)
+> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3)
+> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (19 transition replays, 68 states visited overall)
> [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) From signal: Segmentation fault
> [ 0.000000] (0:maestro@) Counter-example execution trace:
-> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 3)
-> [ 0.000000] (0:maestro@) 1: Random([0;5] ~> 4)
+> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 3)
+> [ 0.000000] (0:maestro@) Actor 1 in simcall Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (19 transition replays, 68 states visited overall)
> [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc