--- from "Efficient Algorithms for Model Checking Pushdown Systems," J. Esparza, et. al. --- This example does not require logical model checking.. --- We only use "bisimilar equational abstraction" to verify --- the desired LTL properties. fmod OPERATION-STACK is sort Operation . ops s m up down right : -> Operation [ctor] . sort Stack . subsort Operation < Stack . op nil : -> Stack [ctor] . op _::_ : Stack Stack -> Stack [ctor assoc id: nil] . endfm mod PLOTTER is pr OPERATION-STACK . sort Conf . op `[_`] : Stack -> Conf [ctor] . var ST : Stack . rl [s1] : [s :: ST] => [ST] . rl [s2] : [s :: ST] => [up :: m :: down :: ST] . rl [m1] : [m :: ST] => [s :: right :: ST] . rl [m2] : [m :: ST] => [s :: right :: m :: ST] . rl [m3] : [m :: ST] => [up :: m :: down :: ST] . rl [d1] : [up :: ST] => [ST] . rl [d2] : [down :: ST] => [ST] . rl [d3] : [right :: ST] => [ST] . endm load model-checker mod PLOTTER-SATISFACTION is pr PLOTTER . pr MODEL-CHECKER . subsort Conf < State . ops up down right : -> Prop [ctor] . var ST : Stack . eq [up :: ST] |= up = true . eq [down :: ST] |= down = true . eq [right :: ST] |= right = true . endm mod PLOTTER-SATISFACTION-ABS is pr PLOTTER-SATISFACTION . vars ST ST' : Stack . eq [ST :: down :: down :: ST'] = [ST :: down :: ST'] . eq [ST :: down :: right :: down :: right :: ST'] = [ST :: down :: right :: ST'] . eq [ST :: m :: down :: right :: m :: down :: right :: ST'] = [ST :: m :: down :: right :: ST'] . --- the equation "eq [ST :: NST :: NST :: ST'] = [ST :: NST :: ST'] ." --- would be used, but it is not confluent. endm set verbose on . --- NOTE: the LTL properties are slightly different from the --- original paper, since our definition of atomic propositions --- only consider the head operation.. That is, even though --- some operation, e.g., "right," is contained in the stack, --- the property "right" can be never satisfied forever. red modelCheck([s],[](up -> (([] ~ right) \/ (~ down U right))) ) . red modelCheck([s],[](down -> (([] ~ right) \/ (~ up U right))) ) .