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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 29 Jan 2023 09:41:21 +0100*References*: <621083e7-5318-4ef6-8fce-fb725ccf806an@googlegroups.com>

In TLA+, the refinement that you want to prove is stated as RefinedSpec => \EE pc : GeneralSpec Unfortunately, no TLA+ verifier handles the \EE quantifier, so you'll have to explain how the pc variable of the high-level spec is implemented in the low-level spec. If you can recompute the value of that variable for any (reachable) state of the low-level spec, you can define that refinement mapping using an operator definition (in the module for the low-level spec) AbstractPC == ... Then instantiate the high-level spec GSpec == INSTANCE HighLevel WITH pc <- AbstractPC and check the property GSpec!Spec. If you cannot come up with the required mapping, you'll need to use history or prophecy variables, and things get more complicated [1,2]. 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/5E7E573C-CCFE-4FD5-9015-C8248A05F562%40gmail.com. |

**References**:**[tlaplus] checking that a pluscal spec implements another pluscal spec***From:*jack malkovick

- Prev by Date:
**Re: [tlaplus] A simple (distinct) states question** - Next by Date:
**[tlaplus] Specifying initial state of a spec while running TLC** - Previous by thread:
**[tlaplus] checking that a pluscal spec implements another pluscal spec** - Next by thread:
**[tlaplus] A simple (distinct) states question** - Index(es):