section‹The state of a firewall, abstracted only to the packet filtering outcome› theory Firewall_Common_Decision_State imports Main begin datatype final_decision = FinalAllow | FinalDeny text‹ The state during packet processing. If undecided, there are some remaining rules to process. If decided, there is an action which applies to the packet › datatype state = Undecided | Decision final_decision end