![]() ![]() This formula should contain neither next-state variables nor input variables. :init true is used to specify the formula for the initial states of the model.All the variables that are not in relation with another by means of a :next attribute are considered inputs. The two variables are linked by annotating x c with the attribute :next x n. For each variable x in the model, the VMT file contains a pair of variables, x c and x n, representing respectively the current and next version of x. :next name is used to represent state variables.More specifically, the following annotations are used: VMT exploits the capability offered by the SMT2 language of attaching annotations to terms and formulas in order to specify the components of the transition system and the properties to verify. ![]()
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |