Quelle  ROOT

chapter AFP

session FSM_Tests = "HOL-Library" +
  options [timeout = 2400]
  sessions
    "Datatype_Order_Generator"
    "Containers"
    "Native_Word"
  directories
    "AdaptiveStateCounting"
    "EquivalenceTesting"
  theories
    "Util"
    "Util_Refined"
    "FSM_Impl"
    "FSM"
    "Product_FSM"
    "Distinguishability"
    "IO_Sequence_Set"
    "Minimisation"
    "Observability"
    "Prefix_Tree"
    "Prefix_Tree_Refined"
    "Prime_Transformation"
    "State_Cover"
    "OFSM_Tables_Refined"

    "EquivalenceTesting/Convergence"
    "EquivalenceTesting/Convergence_Graph"
    "EquivalenceTesting/Empty_Convergence_Graph"
    "EquivalenceTesting/H_Framework"
    "EquivalenceTesting/H_Method_Implementations"
    "EquivalenceTesting/HSI_Method_Implementations"
    "EquivalenceTesting/Intermediate_Frameworks"
    "EquivalenceTesting/Intermediate_Implementations"
    "EquivalenceTesting/Pair_Framework"
    "EquivalenceTesting/Partial_S_Method_Implementations"
    "EquivalenceTesting/Simple_Convergence_Graph"
    "EquivalenceTesting/SPY_Framework"
    "EquivalenceTesting/SPY_Method_Implementations"
    "EquivalenceTesting/SPYH_Method_Implementations"
    "EquivalenceTesting/Test_Suite_Representations_Refined"
    "EquivalenceTesting/Test_Suite_Representations"
    "EquivalenceTesting/W_Method_Implementations"
    "EquivalenceTesting/Wp_Method_Implementations"

    "AdaptiveStateCounting/Adaptive_Test_Case"
    "AdaptiveStateCounting/Backwards_Reachability_Analysis"
    "AdaptiveStateCounting/Helper_Algorithms"
    "AdaptiveStateCounting/Maximal_Path_Trie"
    "AdaptiveStateCounting/R_Distinguishability"
    "AdaptiveStateCounting/State_Preamble"
    "AdaptiveStateCounting/State_Separator"
    "AdaptiveStateCounting/Test_Suite_Calculation"
    "AdaptiveStateCounting/Test_Suite_Calculation_Refined"
    "AdaptiveStateCounting/Test_Suite_IO"
    "AdaptiveStateCounting/Test_Suite"
    "AdaptiveStateCounting/Traversal_Set"

    "FSM_Code_Datatype"
    "Test_Suite_Generator_Code_Export"
  document_files
    "root.tex"
    "root.bib"
  export_files (in "code_export") [2]
    "FSM_Tests.Test_Suite_Generator_Code_Export:code**"