| -------------------------- MODULE DullReservation -------------------------- | |
| EXTENDS Naturals | |
| VARIABLE reservations | |
| Coaches == { "A", "B" } | |
| SeatNumbers == 1..10 | |
| Seats == Coaches \X SeatNumbers | |
| ---- | |
| Reserve == reservations' = reservations \union {{<<"A", 1>>}} | |
| ---- | |
| Init == reservations = {} | |
| Next == Reserve | |
| ---- | |
| TypeCheck == reservations \in SUBSET SUBSET Seats | |
| ============================================================================= |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment