rm -f pan* *.trail *.out mpi-spin-init.c *.err *~
ms -notest -noprobe -nocancel -noanysource -dl -np=2 -buf=2 -req=2 absolute_dl_bad.prom
MPI-Spin version 1.0 of 20-Sep-2007
mscc -DSAFETY
./pan -n
pan: invalid end state (at depth 3)
pan: wrote absolute_dl_bad.prom.trail
(Spin Version 4.2.9 -- 8 February 2007)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 64 byte, depth reached 4, errors: 1
       5 states, stored
       0 states, matched
       5 transitions (= stored+matched)
       0 atomic steps
hash conflicts: 0 (resolved)

4.879 	memory usage (Mbyte)

MPI-Spin memory usage (bytes): 250869
ms -notest -noprobe -nocancel -noanysource -dl -np=2 -buf=2 -req=2 absolute_dl_good.prom
MPI-Spin version 1.0 of 20-Sep-2007
mscc -DSAFETY
./pan -n
(Spin Version 4.2.9 -- 8 February 2007)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 64 byte, depth reached 18, errors: 0
      63 states, stored
      37 states, matched
     100 transitions (= stored+matched)
      28 atomic steps
hash conflicts: 0 (resolved)

4.879 	memory usage (Mbyte)

MPI-Spin memory usage (bytes): 251397
make clean
rm -f pan* *.trail *.out mpi-spin-init.c *.err *~
ms -notest -noprobe -nocancel -noanysource -dl -np=2 -buf=2 -req=2 assertion_good.prom
MPI-Spin version 1.0 of 20-Sep-2007
mscc -DSAFETY
./pan -n
(Spin Version 4.2.9 -- 8 February 2007)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 80 byte, depth reached 29, errors: 0
     110 states, stored
      53 states, matched
     163 transitions (= stored+matched)
      62 atomic steps
hash conflicts: 0 (resolved)

4.879 	memory usage (Mbyte)

MPI-Spin memory usage (bytes): 251397
ms -notest -noprobe -nocancel -noanysource -dl -np=3 -buf=3 -req=3 collective_match_bad.prom
MPI-Spin version 1.0 of 20-Sep-2007
mscc -DSAFETY
./pan -n

Process Descriptors:
Proc 0:
  rank: 0
  pid: 0
  numHandles: 1
Proc 1:
  rank: 1
  pid: 1
  numHandles: 1
Proc 2:
  rank: 2
  pid: 2
  numHandles: 1

Communication record array:
Getting number of records...
numRecords=3
numOutstandingRequests = 3
numBufferedMessages = 0
Record 0:
  id:           4
  next:         NULL
  comm:         -1
  state:        MCR_VISIBLE_SEND_REQ
  source:       0
  dest:         1
  tag:          5
  count:        0
  datatype:     4
  op:           MPI_SUM
  handle:       0
  data:         0x0
  matchHandle:  255
  isFreeable:   0
  isBufferable: 1
  isTestable:   0
  isCancelable: 0
  isProbeable:  0

Record 1:
  id:           2
  next:         NULL
  comm:         -1
  state:        MCR_UNMATCHED_RECV_REQ
  source:       0
  dest:         1
  tag:        MPI_ANY_TAG
  count:        0
  datatype:     3
  op:           MPI_OP_NULL
  handle:       0
  data:         0x0
  isFreeable:   0
  isTestable:   0
  isCancelable: 0
  status:       [source=255,tag=255,size=-1,state=UNDEFINED]

Record 2:
  id:           1
  next:         NULL
  comm:         -1
  state:        MCR_UNMATCHED_RECV_REQ
  source:       1
  dest:         2
  tag:        MPI_ANY_TAG
  count:        0
  datatype:     3
  op:           MPI_OP_NULL
  handle:       0
  data:         0x0
  isFreeable:   0
  isTestable:   0
  isCancelable: 0
  status:       [source=255,tag=255,size=-1,state=UNDEFINED]


pan: assertion violated MPI collective error: send and recv operators differ: MPI_SUM, MPI_OP_NULL (at depth 17)
pan: wrote collective_match_bad.prom.trail
(Spin Version 4.2.9 -- 8 February 2007)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 96 byte, depth reached 17, errors: 1
      12 states, stored
       0 states, matched
      12 transitions (= stored+matched)
       8 atomic steps
hash conflicts: 0 (resolved)

4.879 	memory usage (Mbyte)

MPI-Spin memory usage (bytes): 252981
make clean
rm -f pan* *.trail *.out mpi-spin-init.c *.err *~
ms -notest -noprobe -nocancel -noanysource -dl -np=3 -buf=3 -req=3 dy_buf_good.prom
MPI-Spin version 1.0 of 20-Sep-2007
mscc -DSAFETY
./pan -n
(Spin Version 4.2.9 -- 8 February 2007)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 120 byte, depth reached 191, errors: 0
    3674 states, stored
    4412 states, matched
    8086 transitions (= stored+matched)
   21280 atomic steps
hash conflicts: 10 (resolved)

5.289 	memory usage (Mbyte)

MPI-Spin memory usage (bytes): 259893
make clean
rm -f pan* *.trail *.out mpi-spin-init.c *.err *~
ms -notest -noprobe -nocancel -noanysource -np=3 -dl -buf=3 -req=3 not_single_path_good.prom
MPI-Spin version 1.0 of 20-Sep-2007
mscc -DSAFETY
./pan -n
(Spin Version 4.2.9 -- 8 February 2007)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 120 byte, depth reached 43, errors: 0
    1067 states, stored
    1300 states, matched
    2367 transitions (= stored+matched)
    1590 atomic steps
hash conflicts: 3 (resolved)

4.982 	memory usage (Mbyte)

MPI-Spin memory usage (bytes): 253941
make clean
rm -f pan* *.trail *.out mpi-spin-init.c *.err *~
ms -notest -noprobe -nocancel -noanysource -dl -np=2 -buf=2 -req=2 potential_deadlock_bad.prom
MPI-Spin version 1.0 of 20-Sep-2007
mscc -DSAFETY
./pan -n
pan: invalid end state (at depth 7)
pan: wrote potential_deadlock_bad.prom.trail
(Spin Version 4.2.9 -- 8 February 2007)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 64 byte, depth reached 8, errors: 1
       9 states, stored
       0 states, matched
       9 transitions (= stored+matched)
       0 atomic steps
hash conflicts: 0 (resolved)

4.879 	memory usage (Mbyte)

MPI-Spin memory usage (bytes): 250965
make clean
rm -f pan* *.trail *.out mpi-spin-init.c *.err *~
ms -notest -noprobe -nocancel -noanysource -dl -np=2 -buf=2 -req=2 rbuf_overflow_bad.prom
MPI-Spin version 1.0 of 20-Sep-2007
mscc -DSAFETY
./pan -n

Process Descriptors:
Proc 0:
  rank: 0
  pid: 0
  numHandles: 1
Proc 1:
  rank: 1
  pid: 1
  numHandles: 1

Communication record array:
Getting number of records...
numRecords=2
numOutstandingRequests = 2
numBufferedMessages = 0
Record 0:
  id:           4
  next:         NULL
  comm:         1
  state:        MCR_MATCHED_RECV_REQ
  source:       255
  dest:         1
  tag:          255
  count:        1
  datatype:     3
  op:           MPI_OP_NULL
  handle:       0
  data:         0x103b6f638
  isFreeable:   0
  isTestable:   0
  isCancelable: 0
  status:       [source=255,tag=255,size=-1,state=UNDEFINED]

Record 1:
  id:           5
  next:         NULL
  comm:         1
  state:        MCR_MATCHED_SEND_REQ
  source:       0
  dest:         1
  tag:          0
  count:        2
  datatype:     3
  op:           MPI_OP_NULL
  handle:       0
  data:         0x103b6f61c
  matchHandle:  0
  isFreeable:   0
  isBufferable: 0
  isTestable:   0
  isCancelable: 0
  isProbeable:  0


pan: assertion violated synch: buffer overflow: : sendSize=8, recvCount=1, recvDatumSize=4 (at depth 9)
pan: wrote rbuf_overflow_bad.prom.trail
(Spin Version 4.2.9 -- 8 February 2007)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 96 byte, depth reached 9, errors: 1
      10 states, stored
       0 states, matched
      10 transitions (= stored+matched)
       0 atomic steps
hash conflicts: 0 (resolved)

4.879 	memory usage (Mbyte)

MPI-Spin memory usage (bytes): 251013
make clean
rm -f pan* *.trail *.out mpi-spin-init.c *.err *~
ms -notest -noprobe -nocancel -noanysource -dl -np=4 -buf=4 -req=20 simple_nb_good.prom
MPI-Spin version 1.0 of 20-Sep-2007
mscc -DSAFETY
./pan -n
(Spin Version 4.2.9 -- 8 February 2007)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 408 byte, depth reached 65, errors: 0
   64455 states, stored
  118306 states, matched
  182761 transitions (= stored+matched)
   87820 atomic steps
hash conflicts: 3740 (resolved)

Stats on memory usage (in Megabytes):
27.071	equivalent memory usage for states (stored*(State-vector + overhead))
26.806	actual memory usage for states (compression: 99.02%)
	State-vector as stored = 404 byte + 12 byte overhead
4.194 	memory used for hash table (-w19)
0.480 	memory used for DFS stack (-m10000)
0.201 	memory lost to fragmentation
31.298	total actual memory usage

MPI-Spin memory usage (bytes): 259861
make clean
rm -f pan* *.trail *.out mpi-spin-init.c *.err *~
ms -notest -noprobe -nocancel -noanysource -dl -np=2 -buf=2 -req=2 tags_good.prom
MPI-Spin version 1.0 of 20-Sep-2007
mscc -DSAFETY
./pan -n
(Spin Version 4.2.9 -- 8 February 2007)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 64 byte, depth reached 26, errors: 0
      85 states, stored
      56 states, matched
     141 transitions (= stored+matched)
      63 atomic steps
hash conflicts: 0 (resolved)

4.879 	memory usage (Mbyte)

MPI-Spin memory usage (bytes): 252021
make clean
rm -f pan* *.trail *.out mpi-spin-init.c *.err *~
ms -notest -noprobe -nocancel -noanysource -dl -np=2 -buf=2 -req=2 type_match_p2p_bad.prom
MPI-Spin version 1.0 of 20-Sep-2007
mscc -DSAFETY
./pan -n

Process Descriptors:
Proc 0:
  rank: 0
  pid: 0
  numHandles: 1
Proc 1:
  rank: 1
  pid: 1
  numHandles: 1

Communication record array:
Getting number of records...
numRecords=2
numOutstandingRequests = 2
numBufferedMessages = 0
Record 0:
  id:           4
  next:         NULL
  comm:         1
  state:        MCR_MATCHED_RECV_REQ
  source:       255
  dest:         1
  tag:          255
  count:        1
  datatype:     3
  op:           MPI_OP_NULL
  handle:       0
  data:         0x106d11614
  isFreeable:   0
  isTestable:   0
  isCancelable: 0
  status:       [source=255,tag=255,size=-1,state=UNDEFINED]

Record 1:
  id:           5
  next:         NULL
  comm:         1
  state:        MCR_MATCHED_SEND_REQ
  source:       0
  dest:         1
  tag:          0
  count:        1
  datatype:     1
  op:           MPI_OP_NULL
  handle:       0
  data:         0x106d115fe
  matchHandle:  0
  isFreeable:   0
  isBufferable: 0
  isTestable:   0
  isCancelable: 0
  isProbeable:  0


pan: assertion violated synch: recvDatumSize does not divide sendSize: sendSize=1, recvDatumSize=4 (at depth 7)
pan: wrote type_match_p2p_bad.prom.trail
(Spin Version 4.2.9 -- 8 February 2007)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	+

State-vector 64 byte, depth reached 7, errors: 1
       8 states, stored
       0 states, matched
       8 transitions (= stored+matched)
       0 atomic steps
hash conflicts: 0 (resolved)

4.879 	memory usage (Mbyte)

MPI-Spin memory usage (bytes): 251013
