[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: strange problem with EG operator




Sara:  EG needs an infinite path whereas your transition system
deadlocks at state StateS3.  If you add a self-loop to StateS3
or a transition from StateS3 to StateS1, you should be able
to model check the EG property.

-Shankar

> Hi,
> 
> I have the following simple state space:
> 
> (details are in the attachement)
> 
> C1 with a = true, b = 1
> C2 with a = true, b = 2
> C3 with a = true, b = 3
> 
> and from C1 I can go to C2 and from C2 I can go to C3
> 
> It is very trivial that there exists a path for which a is true in each
> node. However for PVS this is not the case but I do not see where I make a
> mistake. Can anyone explain to me why this is the case?
> 
> (the AG operator works fine, the AF not because it is implemented in
> function of the EG operator)
> 
> Thanks a lot for the help,
> 
> Sara