KATch2 Logo KATch2  Playground

Basic Operations

Tests

x2 == 1 x1 == 0

Assignments

x2 := 1 x2 := 0

Sequential Composition

x2 == 1; x1 := 0 x0 := 1; x2 := 0 x0 == 1; x2 := 0

Choice Operations

x0 := 1 + x1 := 1 (x0 == 1; x1 := 1) + x1 := 0 x0 == 1 + x1 := 0

If-Then-Else

(x0 == 1; x1 := 1) + (x0 == 0; x1 := 0) (x1 == 0; x0 := 1) + (x1 == 1; x0 := 0)

Advanced Operations

Dup (Logging)

x1 := 1; dup; x2 := 1 x0 := 1; dup; x1 := 1; dup

Iteration (Kleene Star)

((x0:=1 + (x0==1;x1:=1) + (x1==1; x2:=1)); dup)* (x0 == 0; x0 := 1)* ((x0 == 0; x0 := 1); dup)* ((x0 := 0 + x0 := 1); dup)*

Logical Operators

Intersection

(x0 == 1) & (x1 == 0)

XOR / Symmetric Difference

(x0 == 1; x1 == 1) ^ (x0 == 1 ; x1 := 1)

Difference

(x0 == 1) - (x1 == 1)

Verification

Subset Check

(x0 == 1) - (x0 == 1 + x1 == 1)

Equality Check

(x0 == 1; x1 == 0) ^ (x1 == 0 & x0 == 1)

Complex Exercises

(x0 == 0; x0 := 1) + (x0 == 1; x0 := 0) (x0 == 1; x1 := 1) + (x0 == 0; x1 := 0) (x0 == 0; x1 == 0) + (x0 == 1; x1 == 1) (x0 == 0; x1 == 1; x0 := 1; x1 := 0) + (x0 == 1; x1 == 0; x0 := 0; x1 := 1) + (x0 == 0; x1 == 0) + (x0 == 1; x1 == 1) // Bit flipper with logging (x0 == 0; x0 := 1 + x0 == 1; x0 := 0); dup; x1 := 1 // Conditional assignment chain x0 == 1; (x1 == 0; x2 := 1 + x1 == 1; x2 := 0); dup (x0 := 1; x1 := 1) ^ (x1 := 1; x0 := 1)

NetKAT Editor

Click an example or exercise from the sidebar to load it, or write your own NetKAT expression

// Welcome to the KATch2 NetKAT Playground! // Click any example or exercise from the sidebar to load it // Or write your own NetKAT expressions here x0 == 1 + x1 := 0 + dup