/** Door example
 *  
 *  Gregor v. Bochmann, December 2008 */

UNLOCKED = (open -> OPEN | lock -> LOCKED),
OPEN = (close -> UNLOCKED),
LOCKED = (unlock -> UNLOCKED).

// TESTCASE1 = (lock -> open -> END).

// TESTCASE2 = (lock -> open -> END)+{unlock, close}.

// ||TEST1 = (UNLOCKED || TESTCASE1).

// ||TEST2 = (UNLOCKED || TESTCASE2).