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