[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Two Questions about (State) Constraints in TLC

Dear all,

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?