[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Two Questions about (State) Constraints in TLC
I have two questions about (state) constraints in TLC:
1. Suppose I want to check Spec => [ ]Property under the state constraint SC in command line mode.
How should I specify the state constraint in command line?
2. Is it possible to impose constraints on the length of the diameter of the reachable-state graph in the model checking mode?