model checking - CTL fomula until contains implication -

when use nusmv tools verify if ctl right, encounter problem make me confused.

my model

and here's nusmv code:

module main var   state : {root, a1, b1, c1, d1, f1, m1};  assign   init(state) := root;    next(state) := case     state = root : a1;     state = a1   : {b1, c1};     state = b1   : d1;     state = d1   : f1;     true : state;   esac;  ctlspec   ag( state=a1 -> ax ( [ state=b1 u ( state=d1 -> ex state=f1 ) ] ) ); ctlspec   ag( state=a1 -> ax ( [ state=b1 u ( state=f1 -> ex state=c1 ) ] ) ); ctlspec   ag( state=a1 -> ax ( [ state=m1 u ( state=f1 -> ex state=c1 ) ] ) ); 

my ctl formula follows:

1. "ag( a1 -> ax ( [ b1 u ( d1 -> ex ( f1) ) ] ) )"
2. "ag( a1 -> ax ( [ b1 u ( f1 -> ex ( c1) ) ] ) )"
3. "ag( a1 -> ax ( [ m1 u ( f1 -> ex ( c1) ) ] ) )"

nusmv verified above 3 formulas of turns out true .

so question why formula 2 , formula 3 turn out true?

this question old, think it's still worth answer, issue might misleading other people.

m, s ⊨ a[ϕuψ] iff paths (s, s2,s3, s4, . ..) s.t. si rt si+1 there state sj s.t. m, sj ⊨ ψ , m, si ⊨ ϕ < j.

so, property verified, ϕ must true until when ψ fires.

notice: a [ false u true ] verified.

now, what's problem properties?

1. the first trivially verified.

2. the second formula requires both paths starting @ b1 , c1 verify a [ b1 u ( f1 -> ex ( c1) ) ]. latter formula means b1 should true until when hit state in f1 -> ex c1 holds. sub-formula can translated !f1 or ex c1, means need hit either state in a. f1 false or state in b. f1 true , there exists next state in c1 true.

   • let's consider path starting @ b1 first:
     • there exists no state in b. verified, since f1 not have successor
     • state d1 verify condition a. path starting in b1.
   • we need verify same property on path starting @ c1. here, state c1 not verify ϕ, verify ψ because condition a. true state too. consequence, a [ b1 u ( f1 -> ex ( c1) ) ] holds.

   since a [ b1 u ( f1 -> ex ( c1) ) ] verified both successors of state a1, second formula verified.

3. the third formula same. time around both of paths starting @ b1 , c1 verify property a [ m1 u ( f1 -> ex ( c1) ) ] because in neither of 2 states f1 immediately true, per condition a. mentioned.