Spec_template.prompt

Translate the following into a TSL specification. Remember, this is what TSL code looks like:

```
always assume {
  (room.somebodyEnters
    -> (!(room.empty) W room.somebodyLeaves)) ;
  ((room.somebodyLeaves && room.empty)
    -> (room.empty W room.somebodyEnters)) ;
  (cm.ready || cm.standby || cm.busy) ;
  (cm.ready -> (!(cm.standby) && !(cm.busy))) ;
  (cm.standby -> (!(cm.busy) && !(cm.ready))) ;
  (cm.busy -> (!(cm.ready) && !(cm.standby))) ;
  ([ cm <- turnOn() ] && cm.standby
    -> X cm.busy U ([ cm <- makeCoffee() ] || [ cm <- turnOff() ] R cm.ready)) ;
  ([ cm <- turnOff() ] && cm.ready
    -> X cm.busy U ([ cm <- turnOn() ] R cm.standby)) ;
  (!(!([ cm <- makeCoffee() ]) || !(cm.ready))
    -> X cm.busy U (cm.finished && ([ cm <- makeCoffee() ] || [ cm <- turnOff() ] R cm.ready)));
  ((p 2 3) && [ g <- 1 ] ->  ! ([ g <- 2 ]) W [ g <- 3 ]);
  ([ g <- 1 ] -> ((! ([ g <- 2 ]) W [ g <- 3 ])));
}

always guarantee {
  room.somebodyEnters
    -> F (cm.ready W (room.somebodyLeaves && room.empty));
}
```

This is a complete listing of all functions and predicates you will need to use to create the spec. Everything else should be basic TSL language operators.

[[FUNCTIONS_AND_PREDICATES_GO_HERE]]

Natural language description:

[[NATURAL_LANGUAGE_SUMMARY_GOES_HERE]]

[[NATURAL_LANGUAGE_DESCRIPTION_GOES_HERE]]