CODEWITHSUNDEEP
spin
a3dsfcv
a3dsfcv

Reputation: 1274

Spin and Promela: never and cycle

I'm running spin in validation mode with the code like below. Got a problem with function called 'never'. While execution it gives me an error that functions inc(), dec() and reset() have never been accomplished. But if i add a cycle, it works great. By documentation, 'never' checks the variables on every step. So, why it does not work without a cycle? 

int x=0
proctype Inc(){
 do
  ::true ->
    if
      ::x<10->x=x+1
    fi
 od
}

proctype Dec(){
 do
  ::true ->
    if
      ::x>0->x=x-1
    fi
 od
}

proctype Reset(){
 do
  ::true ->
   if
    ::x==10->x=0
   fi
 od
}


never {       // if I need this to work, i have to add
  To_Init:    //  this line
    if 
      :: (x<0) || (10<x) -> goto accept
      :: else -> goto To_Init      //  and that line
    fi;
  accept:
}

init{
  run Inc();
  run Dec();
  run Reset();
}

'Never' block, that gives me a warning

never { 
    if 
        :: (x<0) || (10<x) -> goto accept
    fi;
    accept:
}

actually, thats not an error, that's kind of warning, shows unreached in proctype Inc, Dec, Reset, Init. Full warning log is below. 

warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)

(Spin Version 6.2.7 — 2 March 2014)
+ Partial Order Reduction

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

State-vector 28 byte, depth reached 0, errors: 0
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.289 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

unreached in proctype Inc
l31never-no-cycle:6, state 3, "x = (x+1)"
l31never-no-cycle:6, state 4, "((x<10))"
l31never-no-cycle:4, state 6, "(1)"
l31never-no-cycle:9, state 9, "-end-"
(4 of 9 states)
unreached in proctype Dec
l31never-no-cycle:15, state 3, "x = (x-1)"
l31never-no-cycle:15, state 4, "((x>0))"
l31never-no-cycle:13, state 6, "(1)"
l31never-no-cycle:18, state 9, "-end-"
(4 of 9 states)
unreached in proctype Reset
l31never-no-cycle:24, state 3, "x = 0"
l31never-no-cycle:24, state 4, "((x==10))"
l31never-no-cycle:22, state 6, "(1)"
l31never-no-cycle:27, state 9, "-end-"
(4 of 9 states)
unreached in claim never_0
l31never-no-cycle:35, state 6, "-end-"
(1 of 6 states)
unreached in init
l31never-no-cycle:39, state 2, "(run Dec())"
l31never-no-cycle:40, state 3, "(run Reset())"
l31never-no-cycle:41, state 4, "-end-"
(3 of 4 states)

Upvotes: 1

Views: 2338

Answers (1)

GoZoner
GoZoner

Reputation: 70135

A never claim reports an error in two case: 1) an 'accept' cycle is detected, or 2) the never claim completes. A third possibility is if the never claim cannot take a step; this third possibility is the one your code is producing

When your claim was:

never { 
    if 
    :: (x<0) || (10<x) -> goto accept
    fi;
    accept:
}

the initial state has no possible step. That is, the never claim start state is just before the if; from that state where x==0 there is no possible next step.

When there is no possible step in a never claim, the verifier backtracks to a state where a step can be taken. In your case, there is no place to back up to and your verification ends because there is nothing more to do. The verifier then notes that lots of code didn't execute (because, in fact, nothing executed in your model).

You can tell that this is not what you anticipated because of all the unexecuted code. But is it not reported as an error.

For your subsequent case, you added an else. In this case the verifier can take a step in the never claim and thus your verification proceeds.

Upvotes: 5

Related Questions