6 ms·

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 glanc

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.

lou1306 4y ago
(Just for the sake of nitpicking: the term is "liveness") 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 https://doi.org/10.1016/S1571-0661(04)80410-9
- laserbeam 4y ago
  > (Just for the sake of nitpicking: the term is "liveness") I appreciate the nitpick, I'm new to this :).