CODEWITHSUNDEEP
verificationpromela
runov
runov

Reputation: 13

SPIN verifier: cannot prove LTL formulae

I have quite simpe sender-receiver protocol:

#define SZ 4
int sent = 0;
int received = 0;
chan ch = [SZ] of {int};
int varch;
init {
    do
    :: ((len(ch) < SZ) && (received != 1)) ->
        d_step {
        ch ! 1; sent = 1; printf("sent\n");
    }
    :: ((len(ch) == SZ) || ((received == 1) && (len(ch) > 0))) ->
    d_step {
        ch ? varch; received = 1; printf("received\n");
    }
    :: 1 -> /* simulates ramdomness */
       atomic {
          printf("timeout1\n");/*break; */
    }
    od;
}

which sends four packets and then receives them. Then I try to prove property: always send implies eventually receive:

ltl pr { [] ( (sent == 1) -> (<> (received == 1)) ) }

...and nothing happens: SPIN does not find both this property prove and its negation.

Why?

Upvotes: 1

Views: 896

Answers (1)

GoZoner
GoZoner

Reputation: 70175

So, upon quick inspection, the LTL property cannot possibly be satisfied. The LTL property includes always but one viable execution is for the do::od statement to take the /* simulates randomness */ option forever. In that case, no queue will be 'received' and the LTL fails.

My SPIN run confirms the above (I put your code into a file 'sr.pml')

$ spin -a sr.pml
$ gcc -o pan pan.c
$ ./pan -a
pan:1: acceptance cycle (at depth 16)
pan: wrote sr.pml.trail

(Spin Version 6.3.2 -- 17 May 2014)
Warning: Search not completed
    + Partial Order Reduction

Full statespace search for:
    never claim             + (pr)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

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

Stats on memory usage (in Megabytes):
    0.001   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

And then we can see the path with:

$ spin -p -t sr.pml
ltl pr: [] ((! ((sent==1))) || (<> ((received==1))))
starting claim 1
using statement merging
Never claim moves to line 4 [(1)]
  2:    proc  0 (:init::1) sr.pml:8 (state 1)   [(((len(ch)<4)&&(received!=1)))]
  4:    proc  0 (:init::1) sr.pml:9 (state 5)   [ch!1]
  4:    proc  0 (:init::1) sr.pml:10 (state 3)  [sent = 1]
          sent
  4:    proc  0 (:init::1) sr.pml:10 (state 4)  [printf('sent\\n')]
Never claim moves to line 3 [((!(!((sent==1)))&&!((received==1))))]
  6:    proc  0 (:init::1) sr.pml:8 (state 1)   [(((len(ch)<4)&&(received!=1)))]
Never claim moves to line 8 [(!((received==1)))]
  8:    proc  0 (:init::1) sr.pml:9 (state 5)   [ch!1]
  8:    proc  0 (:init::1) sr.pml:10 (state 3)  [sent = 1]
          sent
  8:    proc  0 (:init::1) sr.pml:10 (state 4)  [printf('sent\\n')]
 10:    proc  0 (:init::1) sr.pml:8 (state 1)   [(((len(ch)<4)&&(received!=1)))]
 12:    proc  0 (:init::1) sr.pml:9 (state 5)   [ch!1]
 12:    proc  0 (:init::1) sr.pml:10 (state 3)  [sent = 1]
          sent
 12:    proc  0 (:init::1) sr.pml:10 (state 4)  [printf('sent\\n')]
 14:    proc  0 (:init::1) sr.pml:8 (state 1)   [(((len(ch)<4)&&(received!=1)))]
 16:    proc  0 (:init::1) sr.pml:9 (state 5)   [ch!1]
 16:    proc  0 (:init::1) sr.pml:10 (state 3)  [sent = 1]
          sent
 16:    proc  0 (:init::1) sr.pml:10 (state 4)  [printf('sent\\n')]
  <<<<<START OF CYCLE>>>>>
 18:    proc  0 (:init::1) sr.pml:16 (state 11) [(1)]
          timeout1
 20:    proc  0 (:init::1) sr.pml:18 (state 12) [printf('timeout1\\n')]
spin: trail ends after 20 steps
#processes: 1
        sent = 1
        received = 0
        queue 1 (ch): [1][1][1][1]
        varch = 0
 20:    proc  0 (:init::1) sr.pml:7 (state 14)
 20:    proc  - (pr:1) _spin_nvr.tmp:7 (state 10)
1 processes created

The <<<<<START OF CYCLE>>>> shows sr.pml at line 16 (:: 1 -> ...) executed forever. Also, there are other failures of the LTL. Run the SPIN search with './pan -a -i' to find the shortest trail; it indicates that your LTL isn't finding what you intend to find.

Upvotes: 1

Related Questions