Movatterモバイル変換
[0]ホーム
Model Overview Page
ContentsModel descriptionWhat is the behavior spec?What to check?What is the model?How to run?
This model editor page allows you to make the most common choicesof the parameter values with which TLC is to be run. It contains links to theSpec Options Pagefor specifying additional options for telling TLC what spec behaviors to check and to theTLC Options Page for specifying additionalways to control the execution of TLC. Here are what the different sections of the Model Overviewpage are for.
Enter any text you want here. The first line of the text isdisplayed in theQuick Access window's list of models.The behavior spec is the formula or pair of formulas that describe thepossible behaviors of the system or algorithm you want to check. (SeetheWhat Is A Spec? help page.) There are two ways to write the behavior spec:- Init and Next
- A pair of formulas that specify the initial state and the next-state relation,respectively.
- Single formula
- A single temporal formula of the form
Init /\ [][Next]vars /\ F, where Init is the initial predicate, Next is the next-state relation, vars is the tuple of variables,and F is an optional fairness formula.
The only way to write a behavior spec that includes fairness is with a temporal formula.You can also choose to specifyNo behavior spec. This is the only optionif the spec has no variables. With this option, TLC will just check assumptions andevaluate a constant expression, if you have entered one in theEvaluate Constant Expression sectionof theModel Checking Results Page.
There are three kinds of properties of the behavior spec that TLC can check:Deadlock
Adeadlock is said to occur in a state for which the next-state relationallows no successor states. Termination is deadlock that is not considered an error. If you want the behavior spec to allow termination, then you should uncheck thedeadlock option. (This is not necessary for the spec produced by translating a PlusCal algorithm,because its next-state relation is written in a way that causes TLC not to consider normaltermination to be a deadlock.)Invariants
An invariant is a state predicate that is true of all reachable states--that is, states that can occur in a behavior allowed by the behavior spec. You can includea list of invariants. The checking of each invariant can be enabled or disabledby checking or unchecking its box.Properties
TLC can check if the behavior spec satisfies (implies) a temporal property, whichis expressed as a temporal-logic formula. You can specify a list of such properties,each with a check-box for enabling or disabling its checking.The most basic part of a model is an assignment of values to declared constants. To assign a value to a constant, either double-click on the constant or select it and click on the Edit button. This will raise a pop-up dialog giving you the choiceof three ways to assign a value to it:- Ordinary assignment
- You can set the value of the constant to any constant TLA+ expression thatcontains only symbols defined in the spec. The expression can even includedeclared constants, as long as the value assigned to a constant does not dependon that constant. (If there are circular dependencies, TLC willproduce a Java StackOverflowError error.)
- Model value
- It assigns to the constant a model value of the same name. (SeetheModel Values and Symmetry help page.)
- Set of model values
- You must enter a comma-separated list of legal model-value names,optionally enclosed by
{ and }. You will have the option of making thema symmetry set.Atyped model value is one whose name begins with a letterand an underscore--for example, p_42a. If youenter a set of model values that are not all of the same type,you will have to click Next to continue. You will then be given the choice of specifying a typefor the set you have just entered. For example, if you entered theset {2, a, b} and choose the type t , the constant will be assigned theset {t_2, t_a, t_b} of model values. Note that a number like 2 is not a legal model value.
See theModel Values and Symmetry help page to learn about typed values and symmetry sets.
There are two basic ways to run TLC: locally on the computer running theToolbox and remotely using multiple computers. For local execution, you can choosefrom a small number of useful options. See theTLC Options Page for additional choices of how to run TLC. Remote execution offers the possibility ofgreatly speeding up execution through the use of a network of computers. For information about the remote executionoptions, seeRunning TLC in Distributed Mode.
- Model Values and Symmetry
- Running TLC in Distributed Mode
↑ Creating a Model
[8]ページ先頭