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

Re: TLC fails to invalidate temporal invariant

That makes sense! I suppose we can read my spec as "if a behaviour satisfies Spec, then these invariants are true of that behaviour" and of course if no behaviours satisfy Spec then that statement is true. In this case no behaviours satisfy my spec because TemporalAssumptions and [][Next]_Vars are conjoined and in logical conflict. Do you think it's a good idea to display a warning to the user if TLC finds no behaviours satisfying the spec?