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

Re: TLC fails to invalidate temporal invariant

From: Andrew Helwer <andrew...@xxxxxxxxx>
Date: Wed, 2 May 2018 09:51:19 -0700 (PDT)
References: <2f0a704a-4d8f-412c-a51d-eb29d9218795@googlegroups.com> <606ce3c3-6cf9-4fa6-8cd3-8f5294f3aa57@googlegroups.com>

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?

Follow-Ups:
- Re: [tlaplus] TLC fails to invalidate temporal invariant
  - From: Stephan Merz

References:
- TLC fails to invalidate temporal invariant
  - From: Andrew Helwer
- Re: TLC fails to invalidate temporal invariant
  - From: Ron Pressler

Prev by Date: Re: TLC fails to invalidate temporal invariant
Next by Date: Defining a message in a communication protocol
Previous by thread: Re: TLC fails to invalidate temporal invariant
Next by thread: Re: [tlaplus] TLC fails to invalidate temporal invariant
Index(es):
- Date
- Thread