; @origtpdbfilename ./TRS/HM/t009.trs
; @xtcfilename "./TRS_Standard/HirokawaMiddeldorp_04/t009.xml"
(format TRS)
(fun start 1)
(fun busy 7)
(fun F 0)
(fun closed 0)
(fun stop 0)
(fun false 0)
(fun BF 0)
(fun incorrect 0)
(fun FS 0)
(fun open 0)
(fun up 0)
(fun down 0)
(fun B 0)
(fun empty 0)
(fun correct 0)
(fun S 0)
(fun newbuttons 4)
(fun idle 7)
(fun true 0)
(fun or 2)
(rule (start i) (busy F closed stop false false false i))
(rule (busy BF d stop b1 b2 b3 i) incorrect)
(rule (busy FS d stop b1 b2 b3 i) incorrect)
(rule (busy fl open up b1 b2 b3 i) incorrect)
(rule (busy fl open down b1 b2 b3 i) incorrect)
(rule (busy B closed stop false false false empty) correct)
(rule (busy F closed stop false false false empty) correct)
(rule (busy S closed stop false false false empty) correct)
(rule (busy B closed stop false false false (newbuttons i1 i2 i3 i)) (idle B closed stop false false false (newbuttons i1 i2 i3 i)))
(rule (busy F closed stop false false false (newbuttons i1 i2 i3 i)) (idle F closed stop false false false (newbuttons i1 i2 i3 i)))
(rule (busy S closed stop false false false (newbuttons i1 i2 i3 i)) (idle S closed stop false false false (newbuttons i1 i2 i3 i)))
(rule (busy B open stop false b2 b3 i) (idle B closed stop false b2 b3 i))
(rule (busy F open stop b1 false b3 i) (idle F closed stop b1 false b3 i))
(rule (busy S open stop b1 b2 false i) (idle S closed stop b1 b2 false i))
(rule (busy B d stop true b2 b3 i) (idle B open stop false b2 b3 i))
(rule (busy F d stop b1 true b3 i) (idle F open stop b1 false b3 i))
(rule (busy S d stop b1 b2 true i) (idle S open stop b1 b2 false i))
(rule (busy B closed down b1 b2 b3 i) (idle B closed stop b1 b2 b3 i))
(rule (busy S closed up b1 b2 b3 i) (idle S closed stop b1 b2 b3 i))
(rule (busy B closed up true b2 b3 i) (idle B closed stop true b2 b3 i))
(rule (busy F closed up b1 true b3 i) (idle F closed stop b1 true b3 i))
(rule (busy F closed down b1 true b3 i) (idle F closed stop b1 true b3 i))
(rule (busy S closed down b1 b2 true i) (idle S closed stop b1 b2 true i))
(rule (busy B closed up false b2 b3 i) (idle BF closed up false b2 b3 i))
(rule (busy F closed up b1 false b3 i) (idle FS closed up b1 false b3 i))
(rule (busy F closed down b1 false b3 i) (idle BF closed down b1 false b3 i))
(rule (busy S closed down b1 b2 false i) (idle FS closed down b1 b2 false i))
(rule (busy BF closed up b1 b2 b3 i) (idle F closed up b1 b2 b3 i))
(rule (busy BF closed down b1 b2 b3 i) (idle B closed down b1 b2 b3 i))
(rule (busy FS closed up b1 b2 b3 i) (idle S closed up b1 b2 b3 i))
(rule (busy FS closed down b1 b2 b3 i) (idle F closed down b1 b2 b3 i))
(rule (busy B closed stop false true b3 i) (idle B closed up false true b3 i))
(rule (busy B closed stop false false true i) (idle B closed up false false true i))
(rule (busy F closed stop true false b3 i) (idle F closed down true false b3 i))
(rule (busy F closed stop false false true i) (idle F closed up false false true i))
(rule (busy S closed stop b1 true false i) (idle S closed down b1 true false i))
(rule (busy S closed stop true false false i) (idle S closed down true false false i))
(rule (idle fl d m b1 b2 b3 empty) (busy fl d m b1 b2 b3 empty))
(rule (idle fl d m b1 b2 b3 (newbuttons i1 i2 i3 i)) (busy fl d m (or b1 i1) (or b2 i2) (or b3 i3) i))
(rule (or true b) true)
(rule (or false b) b)