I am trying to model check a simple Promela Model for the following LTL property:
ltl { M[0] U M[1] }
And I'm getting an error, guided simulation on the error trail yields the following output:
ltl ltl_0: (M[0]) U (M[1])
spin: couldn't find claim 2 (ignored)
0 :init ini M[0] = 1
Process Statement M[0] M[1]
0 :init ini M[1] = 0 1 0
Starting net with pid 2
0 :init ini run net() 1 0
spin: trail ends after 4 steps
#processes: 2
4: proc 1 (net) petri:11 (state 13)
4: proc 0 (:init:) petri:25 (state 5)
2 processes created
Exit-Status 0
Now I don't see where "M[0] until M[1]" is violated here. M[0] is set to 1 in the init process, and remains so, until M[1] becomes 1. And the trace ends so early, or I maybe I misunderstand the semantics of "stronguntil" entirely. I am quite confident that this is the case... but what am I doing wrong? Is specifying the LTL inside the Promela file ok?
The model in question is the following (a simple petri net):
#define nPlaces 2
#define nTransitions 2
#define inp1(x1) (x1>0) -> x1--
#define out1(x1) x1++
int M[nPlaces];
int T[nTransitions];
proctype net()
{
do
:: d_step{inp1(M[0])->T[0]++;out1(M[1]);skip}
:: d_step{inp1(M[1])->T[1]++;out1(M[0]);skip}
od
}
init
{
atomic
{
M[0] = 1;
M[1] = 0;
}
run net();
}
ltl { M[0] U M[1] }
Your claim is violated in the initial state (before the init use of atomic). Here is a SPIN verification run (pan -a) with output from the trail file:
ebg@ebg$ spin -a foo.pml
ltl ltl_0: (M[0]) U (M[1])
ebg@ebg$ gcc -o pan pan.c
ebg@ebg$ ./pan -a
pan:1: assertion violated !(( !(M[0])&& !(M[1]))) (at depth 0)
pan: wrote foo.pml.trail
(Spin Version 6.2.4 -- 21 November 2012)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (ltl_0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 36 byte, depth reached 6, errors: 1
4 states, stored (7 visited)
1 states, matched
8 transitions (= visited+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.290 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
ebg@ebg$ spin -p -t foo.pml
ltl ltl_0: (M[0]) U (M[1])
starting claim 2
using statement merging
spin: _spin_nvr.tmp:5, Error: assertion violated
spin: text of failed assertion: assert(!((!(M[0])&&!(M[1]))))
Never claim moves to line 5 [D_STEP]
spin: trail ends after 1 steps
#processes: 1
M[0] = 0
M[1] = 0
T[0] = 0
T[1] = 0
1: proc 0 (:init:) foo.pml:18 (state 3)
1: proc - (ltl_0) _spin_nvr.tmp:3 (state 6)
1 processes created
you can see that the ltl was translated to: assert(!(( !(M[0])&& !(M[1])))) which is:
!(( !0 && !0))
!(( 1 && 1))
!(( 1 ))
0
and thus the assertion is violated.
The easiest way to avoid the problem is to change your arrays to just separate variables. Since your arrays are just size 2 it is easy to do:
int M0 = 1;
int M1 = 0;
int T0 = 0;
int T1 = 0;
/* then use as appropriate. */
With this, you can skip the init and just make the net proctype declared as active proctype net ()