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

Re: [tlaplus] pvs, temporal logic and stacks


My closure axiom is unnecessary as it is covered by the first axiom for push. Also, due to my lack of algebra/logic/model-theory knowledge, I don't understand why your axiom about the uniqueness of S is necessary. Anyway, I think that this exercise proves Leslie's point about the difficulty of the algebraic/axiomatic approach for engineers (like me), not to speak of the difficulty of model-checking such specifications (BTW, are there model checkers for that approach?)