munta/ROOT at master · wimmers/munta · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
session "TA_Library" in "library" = "Refine_Imperative_HOL" +
  sessions
    Transition_Systems_and_Automata
    LTL_Master_Theorem
  theories
    Syntax_Bundles
    ML_Util
    More_Methods
    Abstract_Term
    Instantiate_Existentials
    Reordering_Quantifiers
    More_List
    Stream_More
    Bijective_Embedding
    Tracing
    Printing
    Trace_Timing
    Error_List_Monad
    Imperative_Loops
    Temporal_Logics
    CTL
    Subsumption_Graphs

session DBM in DBM = TA_Library +
  theories
    Floyd_Warshall
    FW_Code
    DBM_Operations
    DBM_Normalization
    DBM_Constraint_Systems
    DBM_Operations_Impl_Refine
    FW_More

session TA in TA = DBM +
  options
    [document = pdf, document_output = "output",
     document_variants = "abstract_reachability_proofs:abstract_reachability=/proof,/ML"]
  theories [document = false]
    Main HOL.Real
  theories
    Normalized_Zone_Semantics
  theories [document = false]
    TA_More
  document_files
    "root.bib" "wasysym.sty"
  document_files (in "document/abstract_reachability")
    "root.tex"

session Worklist_Algorithms in Worklist_Algorithms = TA_Library +
  theories
    Worklist_Subsumption_Impl1
    Unified_PW_Impl
    Liveness_Subsumption_Impl
    Leadsto_Impl
    Worklist_Subsumption_Multiset

session TA_Impl in TA_Impl = TA +
  sessions
    Show
    Worklist_Algorithms
  theories [document = false]
    Refine_Imperative_HOL.IICF
    "HOL-Library.IArray"
  theories
    Normalized_Zone_Semantics_Impl_Refine
    Normalized_Zone_Semantics_Impl_Extra

session Certification in Certification = TA_Impl +
  options
    [quick_and_dirty]
  sessions
    Graph_Theory
  theories
    Lasso_Freeness_Certificates_Complete
    Unreachability_Certification
    Unreachability_Certification2
    Simulation_Graphs2
    TA_Simulation
    Normalized_Zone_Semantics_Certification_Impl
    Normalized_Zone_Semantics_Certification_Impl2

session Networks in Networks = TA_Impl +
  theories
    State_Networks

session Uppaal_Networks in Uppaal_Networks = Networks +
  theories
    UPPAAL_Model_Checking

session Simple_Networks in Simple_Networks = Uppaal_Networks +
  sessions
    FinFun
  theories
    Simple_Network_Language_Model_Checking

session Deadlock in Deadlock = Uppaal_Networks +
  theories
    Deadlock_Checking

session Parsing in Parsing = Certification_Monads +
  sessions
    "HOL-Library"
    Show
  theories
    JSON_Parsing

session TA_Code in Model_Checking = Simple_Networks +
  sessions
    Certification_Monads
    FinFun
    Gabow_SCC
    Deadlock
    Parsing
  theories
    Simple_Network_Language_Export_Code
    Shortest_SCC_Paths

session TA_Certificates in Certificate_Checking = TA_Code +
  options
    [quick_and_dirty]
  theories
    Simple_Network_Language_Certificate_Code