>>>>> "vg" == vanessa goyal <vanessa_goyal@rediffmail.com> writes:
vg> In the example of ARBITER three controllers have register for
vg> passtoken variable. There are no states in which more than one
vg> passtoken will be set. so we can remove such states and reduce
vg> state space. Is it possible in VIS?
No, it is not possible. There are algorithms to detect that some
state variables are expressible as combinations of others. There have
been a couple of experimental implementations in VIS, but none has
been included in the released version thus far.
The earliest work on the subject is probably
@INPROCEEDINGS { Berthe90 ,
AUTHOR = "C. Berthet and O. Coudert and J. C. Madre" ,
BOOKTITLE = iccd ,
MONTH = oct ,
TITLE = "New Ideas on Symbolic Manipulation of Finite State Machines" ,
YEAR = "1990"
}
One of the most recent is:
@INCOLLECTION { Yang99b ,
ADDRESS = "Berlin" ,
AUTHOR = "B. Yang and R. Simmons and R. E. Bryant and D. R. O'Hallaron" ,
BOOKTITLE = "Eleventh Conference on Computer Aided Verification (CAV'99)" ,
EDITOR = "N. Halbwachs and D. Peled" ,
NOTE = "LNCS 1633" ,
PAGES = "328-340" ,
PUBLISHER = "Springer-Verlag" ,
TITLE = "Optimizing Symbolic Model Checking for Constraint-Rich Models" ,
YEAR = "1999"
}
Fabio
This archive was generated by hypermail 2b30 : Sat May 26 2001 - 15:52:37 MDT