Trail replay results in "transition failed" or negative step counts

[mkakh]

When checking the following Promela description, some buggy behaviors appeared.

❯ cat failed.pml
byte i = 0

active [2] proctype process(){
    // transition failed
    (i > 0) -> i--
    // (i > 0) -> i = i - 1

    // OK
    // (i > 0) -> i = - 1
}

1. DFS (default): When checking with DFS, it shows spin: trail ends after -4 steps, but -4 steps is strange.
2. BFS: When checking with BFS, it shows "transition failed" and the counterexample is not correctly displayed.

Especially, the "transition failed" issue troubles me.
When checking a bigger model with an assertion, the same message appeared with the assertion violation, which hinders me to analyze the cause.

I would be grateful for any information regarding a potential workaround or the known cause of this behavior.

The logs are shown the below.

DFS

❯ spin -a failed.pml

❯ gcc -o pan pan.c 

❯ ./pan
pan:1: invalid end state (at depth -1)
pan: wrote failed.pml.trail

(Spin Version 6.5.2 -- 21 June 2024)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	acceptance   cycles 	- (not selected)
	invalid end states	+

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

Stats on memory usage (in Megabytes):
    0.000	equivalent memory usage for states (stored*(State-vector + overhead))
    0.292	actual memory usage for states
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
  128.730	total actual memory usage



pan: elapsed time 0 seconds

❯ spin -t -p failed.pml
spin: trail ends after -4 steps
#processes: 2
		i = 0
 -4:	proc  1 (process:1) failed.pml:5 (state 1)
 -4:	proc  0 (process:1) failed.pml:5 (state 1)
2 processes created

BFS

❯ spin -a failed.pml

❯ gcc -o pan pan.c -DBFS

❯ ./pan
pan:1: invalid end state (at depth 0)
pan: wrote failed.pml.trail

(Spin Version 6.5.2 -- 21 June 2024)
Warning: Search not completed
	+ Breadth-First Search
	+ Partial Order Reduction

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

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

Stats on memory usage (in Megabytes):
    0.000	equivalent memory usage for states (stored*(State-vector + overhead))
    0.292	actual memory usage for states
  128.000	memory used for hash table (-w24)
  128.195	total actual memory usage



pan: elapsed time 0 seconds

❯ spin -t -p failed.pml
  1:	proc  0 (process:1) failed.pml:5 (state 1)	[((i>0))]
	transition failed
spin: trail ends after 1 steps
#processes: 2
		i = 0
  1:	proc  1 (process:1) failed.pml:5 (state 1)
  1:	proc  0 (process:1) failed.pml:5 (state 1)
2 processes created

❯ ./pan -C
spin: trail ends after 1 steps
#processes 2:
  1:	proc 0 (process)  failed.pml:5 (state  1) (invalid end state)
		((i>0))
  1:	proc 1 (process)  failed.pml:5 (state  1) (invalid end state)
		((i>0))
global vars:
	byte   i:	0

Versions

❯ spin -V
Spin Version 6.5.2 -- 21 June 2024

❯ cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=25.04
DISTRIB_CODENAME=plucky
DISTRIB_DESCRIPTION="Ubuntu 25.04"

[nimble-code]

the model is deadlocked in the initial state, so no transition is possible. so the output simply reflects that it is unusual if the model cannot do any transition at all before deadlocking the trail file contains some information about how the verifier was generated. in this case the -4:-4:-4 line indicates that statement merging was used by default (a partial order reduction technique) -- but it ends up being the lonely entry in the trail file, which leads to the odd -4 steps note -- true, that shouldn't be there, but this is a pretty unusual case

…

On Thu, Sep 11, 2025 at 8:26 PM mkakh ***@***.***> wrote: *mkakh* created an issue (nimble-code/Spin#83) <#83> When checking the following Promela description, some buggy behaviors appeared. ❯ cat failed.pml byte i = 0 active [2] proctype process(){ // transition failed (i > 0) -> i-- // (i > 0) -> i = i - 1 // OK // (i > 0) -> i = - 1 } 1. DFS (default): When checking with DFS, it shows spin: trail ends after -4 steps, but -4 steps is strange. 2. BFS: When checking with BFS, it shows "transition failed" and the counterexample is not correctly displayed. Especially, the "transition failed" issue troubles me. When checking a bigger model with an assertion, the same message appeared with the assertion violation, which hinders me to analyze the cause. I would be grateful for any information regarding a potential workaround or the known cause of this behavior. The logs are shown the below. DFS ❯ spin -a failed.pml ❯ gcc -o pan pan.c ❯ ./pan pan:1: invalid end state (at depth -1) pan: wrote failed.pml.trail (Spin Version 6.5.2 -- 21 June 2024) Warning: Search not completed + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + acceptance cycles - (not selected) invalid end states + State-vector 28 byte, depth reached 0, errors: 1 1 states, stored 0 states, matched 1 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 0.292 actual memory usage for states 128.000 memory used for hash table (-w24) 0.534 memory used for DFS stack (-m10000) 128.730 total actual memory usage pan: elapsed time 0 seconds ❯ spin -t -p failed.pml spin: trail ends after -4 steps #processes: 2 i = 0 -4: proc 1 (process:1) failed.pml:5 (state 1) -4: proc 0 (process:1) failed.pml:5 (state 1) 2 processes created BFS ❯ spin -a failed.pml ❯ gcc -o pan pan.c -DBFS ❯ ./pan pan:1: invalid end state (at depth 0) pan: wrote failed.pml.trail (Spin Version 6.5.2 -- 21 June 2024) Warning: Search not completed + Breadth-First Search + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 20 byte, depth reached 0, errors: 1 1 states, stored 1 nominal states (stored-atomic) 0 states, matched 1 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 0.292 actual memory usage for states 128.000 memory used for hash table (-w24) 128.195 total actual memory usage pan: elapsed time 0 seconds ❯ spin -t -p failed.pml 1: proc 0 (process:1) failed.pml:5 (state 1) [((i>0))] transition failed spin: trail ends after 1 steps #processes: 2 i = 0 1: proc 1 (process:1) failed.pml:5 (state 1) 1: proc 0 (process:1) failed.pml:5 (state 1) 2 processes created ❯ ./pan -C spin: trail ends after 1 steps #processes 2: 1: proc 0 (process) failed.pml:5 (state 1) (invalid end state) ((i>0)) 1: proc 1 (process) failed.pml:5 (state 1) (invalid end state) ((i>0)) global vars: byte i: 0 Versions ❯ spin -V Spin Version 6.5.2 -- 21 June 2024 ❯ cat /etc/lsb-release DISTRIB_ID=Ubuntu DISTRIB_RELEASE=25.04 DISTRIB_CODENAME=plucky DISTRIB_DESCRIPTION="Ubuntu 25.04" — Reply to this email directly, view it on GitHub <#83>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AK6L6ILIHHMQ5WLJUWJJSQL3SI4MVAVCNFSM6AAAAACGJUJZB2VHI2DSMVQWIX3LMV43ASLTON2WKOZTGQYDQNRZGYYDKMY> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[mkakh]

Thank you for the reply.

I am still unsure about the cause of the 'transition failed' message.
I apologize for the inconvenience, but I would appreciate your help.

My original intention was to find the cause of this message, which occurs when verifying a larger model. Since the larger model is too complex to analyze directly, I created a minimal model that reproduces the message. I have shared that model here, though the massage only be produced when using the BFS option.

Based on your last reply, I confirmed that the message is shown when a deadlock occurs in the initial state. However, my larger model does not appear to have this kind of deadlock. Furthermore, in the larger model's counterexample, the message appears in the middle of a process's execution, and the process continues to execute steps after the message is shown.

The larger model is available here: https://github.com/tier4/awkernel/tree/92acfbcc2bbf6fe057f634c8ee0280c311304e20/specification/awkernel_async_lib/src/task/preemptive_spin.

The counterexample containing the message is the following. (Full text is here: ce.txt. The trail file is here: preemptive.pml.trail.txt)

1590:   proc  9 (run_main:1) mutex.pml:25 (state 654)   [interrupt_enabled[workers[tid].executing_in] = lock_info[task].interrupt_flag[tid]]
1590:   proc  9 (run_main:1) mutex.pml:26 (state 655)   [lock_info[task].interrupt_flag[tid] = 0]
1590:   proc  9 (run_main:1) mutex.pml:29 (state 658)   [.(goto)]
1592:	proc  9 (run_main:1) preemptive.pml:452 (state 663)	[interrupt_enabled[workers[tid].executing_in] = 1]
                                          future(): tid = 3, task = 0
1594:	proc  9 (run_main:1) future_mock.pml:5 (state 664)	[printf('future(): tid = %d, task = %d\\n',tid,task)]
1596:	proc  9 (run_main:1) future_mock.pml:24 (state 1731)	[((task==1))]
	transition failed
1598:	proc  9 (run_main:1) future_mock.pml:26 (state 1732)	[future_blocked[2] = 1]
1600:	proc  9 (run_main:1) future_mock.pml:26 (state 1733)	[future_blocked[3] = 1]
1602:	proc  9 (run_main:1) future_mock.pml:29 (state 1738)	[poll_result = Ready]
1604:	proc  9 (run_main:1) preemptive.pml:454 (state 1744)	[interrupt_enabled[workers[tid].executing_in] = 0]
                              RUNNING[0] = 3
1606:	proc  6 (run_main:1) preemptive.pml:164 (state 406)	[printf('RUNNING[%d] = %d\\n',workers[tid].executing_in,head)]
1606:	proc  6 (run_main:1) preemptive.pml:166 (state 405)	[RUNNING[workers[tid].executing_in] = head]
Never claim moves to line 21	[(!((!(((((((((((((((waking[0]==0)&&(waking[1]==0))&&(waking[2]==0))&&(waking[3]==0))&&(len(ipi_requests[0])==0))&&(RUNNING[0]!=-(1)))&&(RUNNING[0]!=runnable_preempted_highest_priority))&&(len(ipi_requests[1])==0))&&(RUNNING[1]!=-(1)))&&(RUNNING[1]!=runnable_preempted_highest_priority))&&!(handling_interrupt[0]))&&!(handling_interrupt[1]))&&!(handling_interrupt[2]))&&!(handling_interrupt[3])))||(running_lowest_priority<runnable_preempted_highest_priority))))]
spin: trail ends after 1608 steps

future_mock.pml is available here: https://github.com/tier4/awkernel/blob/1e3a60ead2b52a7c4d35fc3299e677697e47f2f5/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml#L24-L26.

The notable points are

1. proc 9 continues its execution after the 'transition failed' message is displayed.
2. The final report of the model checker is for an assertion violation that occurs elsewhere, not an error related to the 'transition failed' message itself.

We also found that if we change this 'd_step' to 'atomic', the message disappears: https://github.com/tier4/awkernel/blob/92acfbcc2bbf6fe057f634c8ee0280c311304e20/specification/awkernel_async_lib/src/task/preemptive_spin/utility.pml#L25.

---

I found another model that produces the same message, but the cause might be the same as the above minimal model, because it also involves a deadlock.

❯ cat failed2.pml
int i,j

active [5] proctype process() {
    if
    :: i++
    :: i--
    fi;
    if
    :: j++
    :: j--
    fi;
    printf("i: %d, j: %d\n", i, j);
    i == j
}

❯ spin -a failed2.pml

❯ gcc -o pan pan.c -DBFS

❯ ./pan
Depth=      10 States= 2.43e+04 Transitions= 1.14e+05 Memory=   131.125	t=     0.02 R=   1e+06
pan:1: invalid end state (at depth 15)
pan: wrote failed2.pml.trail

(Spin Version 6.5.2 -- 21 June 2024)
Warning: Search not completed
	+ Breadth-First Search
	+ Partial Order Reduction

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

State-vector 52 byte, depth reached 15, errors: 1
    53753 states, stored
	   53753 nominal states (stored-atomic)
   190259 states, matched
   244012 transitions (= stored+matched)
        0 atomic steps
hash conflicts:       212 (resolved)

Stats on memory usage (in Megabytes):
    4.101	equivalent memory usage for states (stored*(State-vector + overhead))
    5.761	actual memory usage for states
  128.000	memory used for hash table (-w24)
  133.664	total actual memory usage



pan: elapsed time 0.05 seconds
pan: rate   1075060 states/second

❯ spin -t -p failed2.pml
  1:	proc  4 (process:1) failed2.pml:5 (state 1)	[i = (i+1)]
  2:	proc  4 (process:1) failed2.pml:9 (state 5)	[j = (j+1)]
                      i: 1, j: 1
  3:	proc  4 (process:1) failed2.pml:12 (state 9)	[printf('i: %d, j: %d\\n',i,j)]
  4:	proc  3 (process:1) failed2.pml:5 (state 1)	[i = (i+1)]
  5:	proc  3 (process:1) failed2.pml:9 (state 5)	[j = (j+1)]
                  i: 2, j: 2
  6:	proc  3 (process:1) failed2.pml:12 (state 9)	[printf('i: %d, j: %d\\n',i,j)]
  7:	proc  2 (process:1) failed2.pml:5 (state 1)	[i = (i+1)]
  8:	proc  2 (process:1) failed2.pml:9 (state 5)	[j = (j+1)]
              i: 3, j: 3
  9:	proc  2 (process:1) failed2.pml:12 (state 9)	[printf('i: %d, j: %d\\n',i,j)]
 10:	proc  1 (process:1) failed2.pml:5 (state 1)	[i = (i+1)]
 11:	proc  1 (process:1) failed2.pml:9 (state 5)	[j = (j+1)]
          i: 4, j: 4
 12:	proc  1 (process:1) failed2.pml:12 (state 9)	[printf('i: %d, j: %d\\n',i,j)]
 13:	proc  0 (process:1) failed2.pml:5 (state 1)	[i = (i+1)]
 14:	proc  0 (process:1) failed2.pml:10 (state 6)	[j = (j-1)]
      i: 5, j: 3
 15:	proc  0 (process:1) failed2.pml:12 (state 9)	[printf('i: %d, j: %d\\n',i,j)]
 16:	proc  0 (process:1) failed2.pml:13 (state 10)	[((i==j))]
	transition failed
spin: trail ends after 16 steps
#processes: 5
		i = 5
		j = 3
 16:	proc  4 (process:1) failed2.pml:13 (state 10)
 16:	proc  3 (process:1) failed2.pml:13 (state 10)
 16:	proc  2 (process:1) failed2.pml:13 (state 10)
 16:	proc  1 (process:1) failed2.pml:13 (state 10)
 16:	proc  0 (process:1) failed2.pml:13 (state 10)
5 processes created

When I add the following process, the 'transition failed' message disappears, since there are no deadlocks:

active proctype monitor() {
	timeout -> i = j; assert(false)

}

---

What is the likely cause of this message in the large model, and what is the recommended way to address it?

[nimble-code]

how did you compile and run the preemptive.pml model?

…

On Sat, Sep 13, 2025 at 9:01 PM mkakh ***@***.***> wrote: *mkakh* left a comment (nimble-code/Spin#83) <#83 (comment)> Thank you for the reply. I am still unsure about the cause of the 'transition failed' message. I apologize for the inconvenience, but I would appreciate your help. My original intention was to find the cause of this message, which occurs when verifying a larger model. Since the larger model is too complex to analyze directly, I created a minimal model that reproduces the message. I have shared that model here, though the massage only be produced when using the BFS option. Based on your last reply, I confirmed that the message is shown when a deadlock occurs in the initial state. However, my larger model does not appear to have this kind of deadlock. Furthermore, in the larger model's counterexample, the message appears in the middle of a process's execution, and the process continues to execute steps after the message is shown. The larger model is available here: https://github.com/tier4/awkernel/tree/92acfbcc2bbf6fe057f634c8ee0280c311304e20/specification/awkernel_async_lib/src/task/preemptive_spin . The counterexample containing the message is the following. (Full text is here: ce.txt <https://github.com/user-attachments/files/22318001/ce.txt>. The trail file is here: preemptive.pml.trail.txt <https://github.com/user-attachments/files/22317979/preemptive.pml.trail.txt> ) 1590: proc 9 (run_main:1) mutex.pml:25 (state 654) [interrupt_enabled[workers[tid].executing_in] = lock_info[task].interrupt_flag[tid]] 1590: proc 9 (run_main:1) mutex.pml:26 (state 655) [lock_info[task].interrupt_flag[tid] = 0] 1590: proc 9 (run_main:1) mutex.pml:29 (state 658) [.(goto)] 1592: proc 9 (run_main:1) preemptive.pml:452 (state 663) [interrupt_enabled[workers[tid].executing_in] = 1] future(): tid = 3, task = 0 1594: proc 9 (run_main:1) future_mock.pml:5 (state 664) [printf('future(): tid = %d, task = %d\\n',tid,task)] 1596: proc 9 (run_main:1) future_mock.pml:24 (state 1731) [((task==1))] transition failed 1598: proc 9 (run_main:1) future_mock.pml:26 (state 1732) [future_blocked[2] = 1] 1600: proc 9 (run_main:1) future_mock.pml:26 (state 1733) [future_blocked[3] = 1] 1602: proc 9 (run_main:1) future_mock.pml:29 (state 1738) [poll_result = Ready] 1604: proc 9 (run_main:1) preemptive.pml:454 (state 1744) [interrupt_enabled[workers[tid].executing_in] = 0] RUNNING[0] = 3 1606: proc 6 (run_main:1) preemptive.pml:164 (state 406) [printf('RUNNING[%d] = %d\\n',workers[tid].executing_in,head)] 1606: proc 6 (run_main:1) preemptive.pml:166 (state 405) [RUNNING[workers[tid].executing_in] = head] Never claim moves to line 21 [(!((!(((((((((((((((waking[0]==0)&&(waking[1]==0))&&(waking[2]==0))&&(waking[3]==0))&&(len(ipi_requests[0])==0))&&(RUNNING[0]!=-(1)))&&(RUNNING[0]!=runnable_preempted_highest_priority))&&(len(ipi_requests[1])==0))&&(RUNNING[1]!=-(1)))&&(RUNNING[1]!=runnable_preempted_highest_priority))&&!(handling_interrupt[0]))&&!(handling_interrupt[1]))&&!(handling_interrupt[2]))&&!(handling_interrupt[3])))||(running_lowest_priority<runnable_preempted_highest_priority))))] spin: trail ends after 1608 steps future_mock.pml is available here: https://github.com/tier4/awkernel/blob/1e3a60ead2b52a7c4d35fc3299e677697e47f2f5/specification/awkernel_async_lib/src/task/preemptive_spin/future_mock.pml#L24-L26 . The notable point are 1. proc 9 continues its execution after the 'transition failed' message is displayed. 2. The final report of the model checker is for an assertion violation that occurs elsewhere, not an error related to the 'transition failed' message itself. We also found that if we change this 'd_step' to 'atomic', the message disappears: https://github.com/tier4/awkernel/blob/92acfbcc2bbf6fe057f634c8ee0280c311304e20/specification/awkernel_async_lib/src/task/preemptive_spin/utility.pml#L25 . ------------------------------ I found another model that produces the same message, but the cause might be the same as the above minimal model, because it also involves a deadlock. ❯ cat failed2.pml int i,j active [5] proctype process() { if :: i++ :: i-- fi; if :: j++ :: j-- fi; printf("i: %d, j: %d\n", i, j); i == j } ❯ spin -a failed2.pml ❯ gcc -o pan pan.c -DBFS ❯ ./pan Depth= 10 States= 2.43e+04 Transitions= 1.14e+05 Memory= 131.125 t= 0.02 R= 1e+06 pan:1: invalid end state (at depth 15) pan: wrote failed2.pml.trail (Spin Version 6.5.2 -- 21 June 2024) Warning: Search not completed + Breadth-First Search + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 52 byte, depth reached 15, errors: 1 53753 states, stored 53753 nominal states (stored-atomic) 190259 states, matched 244012 transitions (= stored+matched) 0 atomic steps hash conflicts: 212 (resolved) Stats on memory usage (in Megabytes): 4.101 equivalent memory usage for states (stored*(State-vector + overhead)) 5.761 actual memory usage for states 128.000 memory used for hash table (-w24) 133.664 total actual memory usage pan: elapsed time 0.05 seconds pan: rate 1075060 states/second ❯ spin -t -p failed2.pml 1: proc 4 (process:1) failed2.pml:5 (state 1) [i = (i+1)] 2: proc 4 (process:1) failed2.pml:9 (state 5) [j = (j+1)] i: 1, j: 1 3: proc 4 (process:1) failed2.pml:12 (state 9) [printf('i: %d, j: %d\\n',i,j)] 4: proc 3 (process:1) failed2.pml:5 (state 1) [i = (i+1)] 5: proc 3 (process:1) failed2.pml:9 (state 5) [j = (j+1)] i: 2, j: 2 6: proc 3 (process:1) failed2.pml:12 (state 9) [printf('i: %d, j: %d\\n',i,j)] 7: proc 2 (process:1) failed2.pml:5 (state 1) [i = (i+1)] 8: proc 2 (process:1) failed2.pml:9 (state 5) [j = (j+1)] i: 3, j: 3 9: proc 2 (process:1) failed2.pml:12 (state 9) [printf('i: %d, j: %d\\n',i,j)] 10: proc 1 (process:1) failed2.pml:5 (state 1) [i = (i+1)] 11: proc 1 (process:1) failed2.pml:9 (state 5) [j = (j+1)] i: 4, j: 4 12: proc 1 (process:1) failed2.pml:12 (state 9) [printf('i: %d, j: %d\\n',i,j)] 13: proc 0 (process:1) failed2.pml:5 (state 1) [i = (i+1)] 14: proc 0 (process:1) failed2.pml:10 (state 6) [j = (j-1)] i: 5, j: 3 15: proc 0 (process:1) failed2.pml:12 (state 9) [printf('i: %d, j: %d\\n',i,j)] 16: proc 0 (process:1) failed2.pml:13 (state 10) [((i==j))] transition failed spin: trail ends after 16 steps #processes: 5 i = 5 j = 3 16: proc 4 (process:1) failed2.pml:13 (state 10) 16: proc 3 (process:1) failed2.pml:13 (state 10) 16: proc 2 (process:1) failed2.pml:13 (state 10) 16: proc 1 (process:1) failed2.pml:13 (state 10) 16: proc 0 (process:1) failed2.pml:13 (state 10) 5 processes created When I add the following process, the 'transition failed' message disappears, since there are no deadlocks: active proctype monitor() { timeout -> i = j; assert(false) } ------------------------------ What is the likely the cause of this message in the large model, and what is the recommended way to address it? — Reply to this email directly, view it on GitHub <#83 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AK6L6IK2HQNCO5CCDDHFGBT3STSDFAVCNFSM6AAAAACGJUJZB2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTEOBZGE3DCOJWG4> . You are receiving this because you commented.Message ID: ***@***.***>

[mkakh]

This is the script that I used:

#!/bin/bash

rm -f "*.trail" pan* {spin-log,pan-log,simple-ce,ce}.txt
$HOME/.local/bin/spin -DSCHED_TYPE_PATTERN=1 -a preemptive.pml 2>&1 > spin-log.txt
gcc -DVECTORSZ=5000 -o pan pan.c
./pan -a -m30000 -Nensure_priority 2>&1 > pan-log.txt

if [ -f "preemptive.pml.trail" ]; then
    $HOME/.local/bin/spin -DSCHED_TYPE_PATTERN=1 -t preemptive.pml 2>&1 > simple-ce.txt
    $HOME/.local/bin/spin -p -DSCHED_TYPE_PATTERN=1 -t preemptive.pml 2>&1 > ce.txt
fi

ce.txt is already shared.
The other files are here:

• spin-log.txt
• pan-log.txt
• simple-ce.txt

This model requires almost 90 GB memory to run.

Since preemptive.pml includes other promela files, they should be stored in the same directory.

[nimble-code]

it is a good question, and you're right for wondering about this. I can reproduce the issue and can see that at the critical point the local variable task (type: short) has the value 0, according to a print statement in the same process: future(): tid = 3, task = 0 and the trail file then continues, believing that task has the value 1 (task==1), which isn't true during the replay, and thus fails. now this is after the assertion failure that reported that a value got truncated (overflowed) -- that truncation/overflow error could have had a different effect during the search than it does during the replay (I'm guessing here), which might explain the difference. I would actually expect the trail to stop as soon as the assertion violation happened, in which case we would not see the issue at all -- so, in short, i'm thinking that the "value truncated in assignment" shortly after the assertion failure put things in a bad state, that causes the hickup later but I have to confess, with this complex of a model, it is hard to be sure -g

…

On Sun, Sep 14, 2025 at 1:26 PM mkakh ***@***.***> wrote: *mkakh* left a comment (nimble-code/Spin#83) <#83 (comment)> This is the script that I used: #!/bin/bash rm -f "*.trail" pan* {spin-log,pan-log,simple-ce,ce}.txt$HOME/.local/bin/spin -DSCHED_TYPE_PATTERN=1 -a preemptive.pml 2>&1 > spin-log.txt gcc -DVECTORSZ=5000 -o pan pan.c ./pan -a -m30000 -Nensure_priority 2>&1 > pan-log.txt if [ -f "preemptive.pml.trail" ]; then $HOME/.local/bin/spin -DSCHED_TYPE_PATTERN=1 -t preemptive.pml 2>&1 > simple-ce.txt $HOME/.local/bin/spin -p -DSCHED_TYPE_PATTERN=1 -t preemptive.pml 2>&1 > ce.txtfi ce.txt is already shared. The other files are here: - spin-log.txt <https://github.com/user-attachments/files/22323436/spin-log.txt> - pan-log.txt <https://github.com/user-attachments/files/22323435/pan-log.txt> - simple-ce.txt <https://github.com/user-attachments/files/22323432/simple-ce.txt> This model requires almost 90 GB memory to run. — Reply to this email directly, view it on GitHub <#83 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AK6L6IJUP5FBODJBW7DOYZ33SXFNVAVCNFSM6AAAAACGJUJZB2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTEOBZHA3DSMJQGE> . You are receiving this because you commented.Message ID: ***@***.***>