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
Left Expression
=
Right Expression
Counterexample (Left ⊃ Right)
Analyzing expressions...
Counterexample (Left ⊂ Right)
Analyzing expressions...
Automata
Left Expression Automaton
Right Expression Automaton
StacKAT Benchmark Report
×

This report shows the performance of the StacKAT equivalence checker with different types of expressions.

All Benchmark Results

Type n Parameter Time (ms) Result