[11] | 1 | |
---|
| 2 | read_fairness - read a fairness constraint |
---|
| 3 | _________________________________________________________________ |
---|
| 4 | |
---|
| 5 | read_fairness [-h] <file> |
---|
| 6 | |
---|
| 7 | Read a fairness constraint, and associate this constraint with the FSM |
---|
| 8 | of the flattened network. An existing constraint associated with the |
---|
| 9 | FSM is lost. Subsequent verification procedures are performed relative |
---|
| 10 | to the new constraint. Note that, by default, the flattened network |
---|
| 11 | has the constraint TRUE, indicating that all paths are fair. The |
---|
| 12 | command build_partition_mdds (or init_verify) must have already been |
---|
| 13 | invoked on the flattened network, before this command is called. |
---|
| 14 | |
---|
| 15 | Currently, only Buchi constraints are supported. A Buchi fairness |
---|
| 16 | constraint is given by a list of individual Buchi conditions, B1, B2, |
---|
| 17 | ..., Bk, where Bi is a set of FSM states. A state is fair if there |
---|
| 18 | exists an infinite path from that state that intersects each Bi |
---|
| 19 | infinitely often. |
---|
| 20 | |
---|
| 21 | The conditions are specified by a file containing at least one CTL |
---|
| 22 | formula (see the [1]VIS CTL and LTL syntax manual). In particular, Bi |
---|
| 23 | is defined by a CTL formula, which represents the set of states that |
---|
| 24 | makes the formula true (in the absence of any fairness constraint). |
---|
| 25 | References to signal names in the network should be made using the |
---|
| 26 | full hierarchical names. Note that the support of any wire referred to |
---|
| 27 | in a formula should consist only of latches. Each CTL formula is |
---|
| 28 | terminated by a semicolon. |
---|
| 29 | |
---|
| 30 | Example: In the three conditions below, B1 contains those states that |
---|
| 31 | have a next state where cntr.out is RED, B2 contains those where |
---|
| 32 | timer.active is 1, and B3 contains those states for which every path |
---|
| 33 | from the state has tlc.request=1 until tlc.acknowledge=1. |
---|
| 34 | |
---|
| 35 | EX(cntr.out=RED); |
---|
| 36 | (timer.active=1); |
---|
| 37 | A(tlc.request=1 U tlc.acknowledge=1); |
---|
| 38 | |
---|
| 39 | |
---|
| 40 | Command options: |
---|
| 41 | |
---|
| 42 | -h |
---|
| 43 | Print the command usage. |
---|
| 44 | |
---|
| 45 | <file> |
---|
| 46 | File containing the set of Buchi conditions. |
---|
| 47 | _________________________________________________________________ |
---|
| 48 | |
---|
| 49 | Last updated on 20050519 10h16 |
---|
| 50 | |
---|
| 51 | References |
---|
| 52 | |
---|
| 53 | 1. file://localhost/projects/development/hsv/vis/common/doc/ctl/ctl/ctl.html |
---|