StacKAT (original) (raw)

StacKAT Playground

In this playground you can enter two StacKAT expressions and see if they are equivalent. If they are inequivalent, the playground will show counter examples. Verify that this correctly implements a decision procedure for the semantics of Figure 1 in the paper.

Expression Syntax:

0 Drop packet

1 Do nothing

push(n) Push value n onto the stack

pop(n) Pop value n from the stack

x:=n Set packet header x to n

x==n Test if packet header x equals n

x!=n Test if packet header x does not equal n

e+e Nondeterministic choice between expressions

e e Sequence: do first expression followed by second

e* Kleene star: repeat expression zero or more times