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

*From*: "cf Shi." <shichunfeng1314@xxxxxxxxx>*Date*: Sun, 25 Jul 2021 19:29:59 -0700 (PDT)

Hello,

I'm new in tlaps and trying to finish the example

I have no idea on it, and whether I handled it in a disorderly way? How to prove RealInv' in the example "BubbleSort" ?

My approach to this is as follows: (of course, this is predictably not working)

<2>2. RealInv'

<3>1. CASE pc = "Lbl_1"

BY DEF TypeOK, RealInv, Lbl_1,

Lbl_2, IsSortedTo,IsSorted,IsSortedFromTo, IsPermOf, Perms, **

<3>2. CASE pc = "Lbl_2"

<3>3. CASE pc = "Done"

BY IsPermOfExchange DEF TypeOK, RealInv, Lbl_1, Lbl_2,IsSortedTo,

IsSorted,IsSortedFromTo, IsPermOf, Perms, **

<3>4. QED

BY <3>1,<3>2,<3>3 DEF TypeOK, RealInv, Lbl_1, Lbl_2

-------------------------------------------------------------------------

[1] https://github.com/tlaplus/tlapm/blob/master/examples/BubbleSort.tla

--

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/ee395ae0-b749-4f4e-9da0-611f91564424n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] How to prove RealInv' in the example "BubbleSort" ?***From:*Stephan Merz

- Prev by Date:
**[tlaplus] Model checking a mutually recursive definition of a tree** - Next by Date:
**Re: [tlaplus] How to prove RealInv' in the example "BubbleSort" ?** - Previous by thread:
**Re: [tlaplus] Re: Model checking a mutually recursive definition of a tree** - Next by thread:
**Re: [tlaplus] How to prove RealInv' in the example "BubbleSort" ?** - Index(es):