(STRATEGY INNERMOST) (VAR b b1 b2 b3 d fl i i1 i2 i3 m) (DATATYPES A = µX.< F, closed, stop, false, BF, incorrect, FS, open, up, down, B, empty, correct, S, newbuttons(X, X, X, X), true >) (SIGNATURES start :: [A] -> A busy :: [A x A x A x A x A x A x A] -> A idle :: [A x A x A x A x A x A x A] -> A or :: [A x A] -> A) (RULES start(i) -> busy(F() ,closed() ,stop() ,false() ,false() ,false() ,i) busy(BF() ,d ,stop() ,b1 ,b2 ,b3 ,i) -> incorrect() busy(FS() ,d ,stop() ,b1 ,b2 ,b3 ,i) -> incorrect() busy(fl ,open() ,up() ,b1 ,b2 ,b3 ,i) -> incorrect() busy(fl ,open() ,down() ,b1 ,b2 ,b3 ,i) -> incorrect() busy(B() ,closed() ,stop() ,false() ,false() ,false() ,empty()) -> correct() busy(F() ,closed() ,stop() ,false() ,false() ,false() ,empty()) -> correct() busy(S() ,closed() ,stop() ,false() ,false() ,false() ,empty()) -> correct() busy(B() ,closed() ,stop() ,false() ,false() ,false() ,newbuttons(i1,i2,i3,i)) -> idle(B() ,closed() ,stop() ,false() ,false() ,false() ,newbuttons(i1,i2,i3,i)) busy(F() ,closed() ,stop() ,false() ,false() ,false() ,newbuttons(i1,i2,i3,i)) -> idle(F() ,closed() ,stop() ,false() ,false() ,false() ,newbuttons(i1,i2,i3,i)) busy(S() ,closed() ,stop() ,false() ,false() ,false() ,newbuttons(i1,i2,i3,i)) -> idle(S() ,closed() ,stop() ,false() ,false() ,false() ,newbuttons(i1,i2,i3,i)) busy(B() ,open() ,stop() ,false() ,b2 ,b3 ,i) -> idle(B() ,closed() ,stop() ,false() ,b2 ,b3 ,i) busy(F() ,open() ,stop() ,b1 ,false() ,b3 ,i) -> idle(F() ,closed() ,stop() ,b1 ,false() ,b3 ,i) busy(S() ,open() ,stop() ,b1 ,b2 ,false() ,i) -> idle(S() ,closed() ,stop() ,b1 ,b2 ,false() ,i) busy(B() ,d ,stop() ,true() ,b2 ,b3 ,i) -> idle(B() ,open() ,stop() ,false() ,b2 ,b3 ,i) busy(F() ,d ,stop() ,b1 ,true() ,b3 ,i) -> idle(F() ,open() ,stop() ,b1 ,false() ,b3 ,i) busy(S() ,d ,stop() ,b1 ,b2 ,true() ,i) -> idle(S() ,open() ,stop() ,b1 ,b2 ,false() ,i) busy(B() ,closed() ,down() ,b1 ,b2 ,b3 ,i) -> idle(B() ,closed() ,stop() ,b1 ,b2 ,b3 ,i) busy(S() ,closed() ,up() ,b1 ,b2 ,b3 ,i) -> idle(S() ,closed() ,stop() ,b1 ,b2 ,b3 ,i) busy(B() ,closed() ,up() ,true() ,b2 ,b3 ,i) -> idle(B() ,closed() ,stop() ,true() ,b2 ,b3 ,i) busy(F() ,closed() ,up() ,b1 ,true() ,b3 ,i) -> idle(F() ,closed() ,stop() ,b1 ,true() ,b3 ,i) busy(F() ,closed() ,down() ,b1 ,true() ,b3 ,i) -> idle(F() ,closed() ,stop() ,b1 ,true() ,b3 ,i) busy(S() ,closed() ,down() ,b1 ,b2 ,true() ,i) -> idle(S() ,closed() ,stop() ,b1 ,b2 ,true() ,i) busy(B() ,closed() ,up() ,false() ,b2 ,b3 ,i) -> idle(BF() ,closed() ,up() ,false() ,b2 ,b3 ,i) busy(F() ,closed() ,up() ,b1 ,false() ,b3 ,i) -> idle(FS() ,closed() ,up() ,b1 ,false() ,b3 ,i) busy(F() ,closed() ,down() ,b1 ,false() ,b3 ,i) -> idle(BF() ,closed() ,down() ,b1 ,false() ,b3 ,i) busy(S() ,closed() ,down() ,b1 ,b2 ,false() ,i) -> idle(FS() ,closed() ,down() ,b1 ,b2 ,false() ,i) busy(BF() ,closed() ,up() ,b1 ,b2 ,b3 ,i) -> idle(F() ,closed() ,up() ,b1 ,b2 ,b3 ,i) busy(BF() ,closed() ,down() ,b1 ,b2 ,b3 ,i) -> idle(B() ,closed() ,down() ,b1 ,b2 ,b3 ,i) busy(FS() ,closed() ,up() ,b1 ,b2 ,b3 ,i) -> idle(S() ,closed() ,up() ,b1 ,b2 ,b3 ,i) busy(FS() ,closed() ,down() ,b1 ,b2 ,b3 ,i) -> idle(F() ,closed() ,down() ,b1 ,b2 ,b3 ,i) busy(B() ,closed() ,stop() ,false() ,true() ,b3 ,i) -> idle(B() ,closed() ,up() ,false() ,true() ,b3 ,i) busy(B() ,closed() ,stop() ,false() ,false() ,true() ,i) -> idle(B() ,closed() ,up() ,false() ,false() ,true() ,i) busy(F() ,closed() ,stop() ,true() ,false() ,b3 ,i) -> idle(F() ,closed() ,down() ,true() ,false() ,b3 ,i) busy(F() ,closed() ,stop() ,false() ,false() ,true() ,i) -> idle(F() ,closed() ,up() ,false() ,false() ,true() ,i) busy(S() ,closed() ,stop() ,b1 ,true() ,false() ,i) -> idle(S() ,closed() ,down() ,b1 ,true() ,false() ,i) busy(S() ,closed() ,stop() ,true() ,false() ,false() ,i) -> idle(S() ,closed() ,down() ,true() ,false() ,false() ,i) idle(fl,d,m,b1,b2,b3,empty()) -> busy(fl,d,m,b1,b2,b3,empty()) 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) or(true(),b) -> true() or(false(),b) -> b)