type ReqType = 		enumeration of extup, extdown, inside 
type Direction = 	enumeration of up, down, none

automaton Elevator
assumes Floors

signature
	input request(t: ReqType, f: Floor) where
 		(t=extup => (f ~= 6)) /\ (t=extdown => (f ~= K))
	output  opendoor(f: Floor),
		closedoor(f : Floor),
		moveup,
		movedown
	states
		floor: 		Floor := B,
	        requests: 	Array[ReqType, Floor, Bool] := constant(false),
		dooropen: 	Array[Floor, Bool] := constant(false),
		direction: 	Direction := none

	transitions
		input request(t,f)
			eff if ~ dooropen[f] then requests[t,f] := true fi;
			if direction=none /\ floor ~= f then
				if f < floor  then direction := down
					       else direction := up fi
			fi

		output opendoor(f)
			pre floor=f /\ dooropen[f]=false /\
			  (requests[inside,f] = true \/
			    (requests[extup,f] = true /\ direction ~= down) \/
			    (requests[extdown,f] = true /\ direction ~= up))
			eff dooropen[f] := true;
			    requests[extup,f] := false;
			    requests[extdown,f] := false;
			    requests[inside,f] := false

		output closedoor(f)
			pre dooropen[f] = true
			eff dooropen[f] := false

		output moveup
			pre dooropen[floor] = false /\ direction = up /\
			    requests[inside,floor] = false /\
			    requests[extup,floor] = false
			eff floor := succ(floor);
			    if \E t: ReqType \E f: Floor
				 (floor < f /\ requests[t,f] = true)
			    then direction := up
 			    else if \E t: ReqType \E f: Floor
				    (f < floor /\ requests[t,f] = true)
			         then direction := down
				 else direction := none
				 fi
			    fi

		output movedown
			pre dooropen[floor] = false /\ direction = down /\
			    requests[inside,floor] = false /\
			    requests[extdown,floor] = false
			eff floor := pred(floor);
			    if \E t: ReqType \E f: Floor
				 (f < floor /\ requests[t,f] = true)
			    then direction := down
 			    else if \E t: ReqType \E f: Floor
				    (floor < f /\ requests[t,f] = true)
			         then direction := up
				 else direction := none
				 fi
			    fi