chapter AFP

session Iptables_Semantics = Routing +
  options [timeout = 1200]
  sessions
    Native_Word
  directories
    "Common"
    "Semantics_Ternary"
    "Primitive_Matchers"
    "Simple_Firewall"
  theories [document = false]
    "Common/List_Misc"
    "Common/WordInterval_Lists"
  theories
    Semantics
    Example_Semantics
    Alternative_Semantics
    Semantics_Stateful
    Semantics_Goto
    Call_Return_Unfolding
    "Common/Negation_Type_DNF"
    "Semantics_Ternary/Semantics_Ternary"
    Matching_Embeddings
    Semantics_Embeddings
    Iptables_Semantics
    Semantics_Stateful
    "Semantics_Ternary/Optimizing"
    "Primitive_Matchers/No_Spoof"
    "Primitive_Matchers/Parser6"
    No_Spoof_Embeddings
    "Primitive_Matchers/Routing_IpAssmt"
    "Primitive_Matchers/Transform"
    "Primitive_Matchers/Primitive_Abstract"
    "Primitive_Matchers/Code_Interface"
    "Primitive_Matchers/Parser"
    "Simple_Firewall/SimpleFw_Compliance"
    Code_haskell
    Access_Matrix_Embeddings
    No_Spoof_Embeddings
    Documentation
  document_files
    "root.tex"
    "root.bib"

session Iptables_Semantics_Examples in "Examples" = Iptables_Semantics +
  options [timeout = 2400]
  directories
    "Parser_Test"
    "Fail"
    "Contrived"
    "Synology_Diskstation_DS414"
    "Ringofsaturn_com"
    "SQRL_Shorewall"
    "sns.ias.edu"
    "medium-sized-company"
  theories
    "Parser_Test/Parser_Test"
    "Parser_Test/Parser6_Test"
    "Small_Examples"
    "Fail/Ports_Fail"
    "Contrived/Contrived_Example"
    "Synology_Diskstation_DS414/Analyze_Synology_Diskstation"
    "Ringofsaturn_com/Analyze_Ringofsaturn_com"
    "SQRL_Shorewall/Analyze_SQRL_Shorewall"
    "SQRL_Shorewall/SQRL_2015_nospoof"
    "sns.ias.edu/SNS_IAS_Eduroam_Spoofing"
    "medium-sized-company/Analyze_medium_sized_company"
  document_files (in "../document")
    "root.tex"
    "root.bib"

session Iptables_Semantics_Examples_Big (slow very_slow) in "Examples_Big" = Iptables_Semantics_Examples +
  options [timeout = 60000]
  directories
    "../Examples/IPPartEval"
    "../Examples/TUM_Net_Firewall"
    "../Examples/containern"
    "../Examples/topoS_generated"
  theories
    "../Examples/topoS_generated/Analyze_topos_generated"
    "../Examples/IPPartEval/IP_Address_Space_Examples_All_Small"
    "../Examples/TUM_Net_Firewall/Analyze_TUM_Net_Firewall"
    "../Examples/containern/Analyze_Containern"
    "../Examples/TUM_Net_Firewall/TUM_Spoofing_new3"
    "../Examples/TUM_Net_Firewall/TUM_Simple_FW"
    "../Examples/IPPartEval/IP_Address_Space_Examples_All_Large"
  document_files (in "../document")
    "root.tex"
    "root.bib"