Spec_withoutAssumptions_template.prompt

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

```
always assume{
}

always guarantee{
//rotate the cube with the value of t (increments by 1 every frame)
    [cube.rotation.y <- t];
}
```

```
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)));
}

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]]