| Thanks for the nice example. I have not looked at the background material and can therefore not comment on the extent to which your spec represents Brunelleschi's hoist. Just a few observations about the TLA+: 1. If Z has to be <<0,0,1>> it would be more appropriate to define it like this Z == <<0,0,1>> instead of declaring it as a constant. Also, it is a little strange to include the predicate InvZ in the invariant, since its value cannot change over a behavior: it only mentions constant Z. The above definition eliminates the need for having InvZ as part of the invariant; alternatively, you could include an assumption ASSUME InvZ == Z = <<0,0,1>> which would be useful if the constant Z could take more than one value but still had to satisfy some predicate. In fact, the relevance of including Z in the specification is not clear to me as it does not play a role in the dynamics of the system (it only occurs in the formula InvZ). I presume you mentally simplified your definitions (such as of Det) taking into account the fixed value of Z. 2. The tools supporting TLA+ do not really support real numbers. In your case, you only have integer vectors (moreover, with a single component equal to 1 or -1 and the others equal to 0), so everything works out fine, but a generalization to actual real numbers would quickly result in failures of model checking or proof. 3. TLC is a model checker. I am assuming you used it before you started writing proofs (for example by instantiating the constant parameter Z and telling TLC to check the invariant Inv). It will tell you that the invariant holds, and that your spec generates 4 reachable states. For such a small finite state space, this is an exhaustive verification technique. TLC actually ignores any THEOREM statements and proofs a module contains: it computes the graph of reachable states and checks properties on that graph. The proofs that you wrote were checked by TLAPS, the TLA+ proof system (an interactive proof assistant). Your style of USEing all relevant defined operators and then writing OBVIOUS works for small formulas. For larger formulas, you want to selectively expand the operators that are really necessary for a given step in order to control the search space of the provers. As you observe, theorem ThType is an immediate corollary of theorem ThInv. You can simplify its proof as follows: THEOREM ThType == Spec => []Typing(x) /\ []Typing(y) <1>. Inv => Typing(x) /\ Typing(y) BY DEF Inv, InvX, InvY, Typing <1>. QED BY ThInv, PTL Thanks again, Stephan
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/7D4630C9-6443-446E-9639-F33095F06B84%40gmail.com. |