← Back to branch summary

~ubuntu-branches/ubuntu/raring/simgrid/raring

« back to all changes in this revision

Viewing changes to examples/msg/mc/chord/chord_neverjoin.tesh

  • Committer: Package Import Robot
  • Author(s): Martin Quinson
  • Date: 2013-01-31 00:24:51 UTC
  • mfrom: (10.1.6 sid)
  • Revision ID: package-import@ubuntu.com-20130131002451-krejhf7w7h24lpsc
Tags: 3.9~rc1-1
* New upstream release: the "Grasgory" release. Major changes:
  - Gras was completely removed from this version.
  - Documentation reorganization to ease browsing it.
  - New default value for the TCP_gamma parameter: 4MiB

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/msg/mc/chord/chord_neverjoin.tesh
 
1
#! ./tesh
 
2
 
 
3
! expect signal SIGABRT
 
4
! timeout 200
 
5
$ ${bindir:=.}/chord_liveness --cfg=model-check:1 --cfg=contexts/factory:ucontext "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
 
6
> [  0.000000] (0:@) Configuration change: Set 'model-check' to '1'
 
7
> [  0.000000] (0:@) Check the liveness property promela_chord_liveness
 
8
> [  0.000000] (1:node@Jean_Yves) Joining the ring with id 14, knowing node 1
 
9
> [  0.000000] (2:node@Boivin) Joining the ring with id 8, knowing node 1
 
10
> [  0.000000] (3:node@Jacquelin) A transfer has occured
 
11
> [  0.000000] (3:node@Jacquelin) The task was successfully received by node 1
 
12
> [  0.000000] (1:node@Jean_Yves) Node 14 joined the ring
 
13
> [  0.000000] (0:@) Next pair (depth = 12, 2 interleave) already reached !
 
14
> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 
15
> [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 
16
> [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 
17
> [  0.000000] (0:@) Counter-example that violates formula :
 
18
> [  0.000000] (0:@) [(1)node] iSend (src=node, buff=(verbose only), size=(verbose only))
 
19
> [  0.000000] (0:@) [(2)node] iSend (src=node, buff=(verbose only), size=(verbose only))
 
20
> [  0.000000] (0:@) [(3)node] iRecv (dst=node, buff=(verbose only), size=(verbose only))
 
21
> [  0.000000] (0:@) [(1)node] Wait (comm=(verbose only) [(1)node -> (3)node])
 
22
> [  0.000000] (0:@) [(1)node] iRecv (dst=node, buff=(verbose only), size=(verbose only))
 
23
> [  0.000000] (0:@) [(3)node] Test TRUE (comm=(verbose only) [(1)node -> (3)node])
 
24
> [  0.000000] (0:@) [(3)node] iSend (src=node, buff=(verbose only), size=(verbose only))
 
25
> [  0.000000] (0:@) [(1)node] Wait (comm=(verbose only) [(3)node -> (1)node])
 
26
> [  0.000000] (0:@) [(1)node] iRecv (dst=node, buff=(verbose only), size=(verbose only))
 
27
> [  0.000000] (0:@) [(1)node] Test FALSE (comm=(verbose only))
 
28
> [  0.000000] (0:@) [(1)node] Test FALSE (comm=(verbose only))
 
29
> [  0.000000] (0:@) Expanded pairs = 16
 
30
> [  0.000000] (0:@) Visited pairs = 11
 
31
> [  0.000000] (0:@) Expanded / Visited = 0.687500
 
 
b'\\ No newline at end of file'