netkat_negation.maude

fmod FIELD is
	protecting NAT .
	sort Field .
endfm

fmod PREDICATE is	
	protecting FIELD .
	protecting NAT .

	sort Predicate .

	op one : -> Predicate [ctor] .
	op zero : -> Predicate [ctor] .	

	op _=_ : Field Nat -> Predicate [ctor metadata "test" prec 39] .
	op ~_ : Predicate -> Predicate [ctor metadata "negation" prec 38] .
	op _+_ : Predicate Predicate -> Predicate [ctor assoc comm metadata "union" prec 43] .
	op _._ : Predicate Predicate -> Predicate [ctor assoc comm metadata "sequential composition" prec 40] .
	
	vars A B : Predicate .
	eq ~ (A + B) = ~ A . ~ B .
	eq ~ (A . B) = ~ A + ~ B .
	
	eq ~ zero = one .
	eq ~ one = zero .
endfm


fmod POLICY is
	protecting FIELD .
	protecting NAT .
	protecting PREDICATE .

	sort Policy .

	op _+_ : Policy Policy -> Policy [ctor assoc comm metadata "union" prec 43] .
	op _._ : Policy Policy -> Policy [ctor assoc metadata "sequential composition" prec 40] .
	op _<-_ : Field Nat -> Policy [ctor metadata "modification" prec 39] .
endfm