fact: Definition ClassifierSpec : ADT ClassifierSig := Def ADT { rep := QueryStructure ClassifierSchema, Def Constructor0 "Init" : rep := empty,, Def Method1 "AddRule" (r : rep) (rule : RuleRecord) : rep * bool := Insert rule into r!RULES, Def Method1 "Classify" (r : rep) (p : Packet) : rep * list RuleRecord := rules <- For (rule in r!RULES) Where (IsPrefix rule!DESTINATION (destination p) /\ FollowPolicy rule!PROTOCOL (protocol p)) Return rule; ret (r, rules) }%methDefParsing.
imports: Fiat.QueryStructure.Automation.MasterPlan