|
|
|
|
|
|
by laserbeam
1205 days ago
|
|
|
My only knowledge on modeling languages is: TLA+ exists, I've seen Lamport's introductory videos/course, I've followed along to the course examples. At a glance, I like that this looks more approachable to write, and I like that. Can it still be used to prove properties like liveliness? The fact that Fault seems to use bounded loops seems counter-intuitive to proving those "x eventually happens" conditions. As I understand (from a distance) you can model those in TLA+. PS. The question regards the design of Fault, not the current state of implementation. |
|
|
Short answer is no (seemingly). From the docs it seems Fault only supports assertions. Finding an assertion violation is a reachability problem and is immediately usable to prove safety problems, not liveness.
But, long answer is "kind of"!
That a counterexample to a liveness property ("x eventually happens") generally is a lasso-shaped execution (so a prefix + a cycle) where x never happens. With that in mind, you can reduce liveness checking to reachability: the only problem is, you have to add state-tracking to your model and assert "the system never closes a cycle when x never happens".
This is explained in detail, e.g., in Armin Biere, Cyrille Artho, and Viktor Schuppan. 2002. Liveness Checking as Safety Checking. Electron. Notes Theor. Comput. Sci. 66, 2 (2002), 160–177. DOI:https://doi.org/10.1016/S1571-0661(04)80410-9