You also know that a reachability property such as the one that you describe can be checked in a linear-time formalism using inverted logic – that is, by asserting the invariant that an accepting state is never reached (in any run of the automaton for the given input string, or equivalently that no application of the CFG rules matches the string), and expecting the model checker to produce a counter example, which exhibits an accepting run / sequence of rule applications. Why is this approach unsuitable for what you are after?
This works for simple reachability properties but doesn't compose
with the other operators well. I can't write []Reachable(Shutdown)
to say that we can always reach the Shutdown state from
every point in the state space, or [](A => Reachable(B)),
etc. Also, it means I can't check two reachability properties in
the same model run.
I don't know if Reachable is worth adding, in particular I don't know if it would interact well with refinement. Just pointing out that inverted logic doesn't fully capture reachability properties!
H
----On 15 Oct 2024, at 16:25, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
All the temporal operators we have ([], <>, ~>) implicitly quantify over all behaviors generated by a spec. So when we check really what we are saying
<>P
really what we are checking is roughly:
\A behavior \in BehaviorsOf(Spec) : \E state \in behavior : P
But what if I only care that at least one behavior generated by the spec satisfies <>P? Something like:
\E behavior \in BehaviorsOf(Spec) : \E state \in behavior : P
Currently, you can only do this by tracking nondeterministic system behaviors in a variable contained within the spec itself, then writing a universally-quantified temporal operator over the value of that variable. However, it would be interesting if this could be offloaded to the model-checker.
This idea was inspired by me specifying nondeterministic finite automatons and context-free grammars as part of an experiment in using TLA+ for undergraduate computer science coursework. A CFG accepts a given string w if some application of the grammar production rules results in string w. If I wanted to model-check to ensure a given CFG accepts a string w, I would need to say that there exists some behavior by the CFG resulting in a string composed entirely of terminals and matching w.
What do people think?
Andrew Helwer
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/efa1d2e9-85d3-4a44-a563-c18832cf23cfn%40googlegroups.com.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BE0249E6-60BB-4E4D-B137-94A70C3A9313%40gmail.com.