-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathConcept_MonitorTest1.thy
127 lines (98 loc) · 4.81 KB
/
Concept_MonitorTest1.thy
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
123
124
125
126
127
(*************************************************************************
* Copyright (C)
* 2019-2023 The University of Exeter
* 2018-2023 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
* This program can be redistributed and/or modified under the terms
* of the 2-clause BSD-style license.
*
* SPDX-License-Identifier: BSD-2-Clause
*************************************************************************)
chapter\<open>Testing Nested Monitors\<close>
theory
Concept_MonitorTest1
imports
"Isabelle_DOF_Unit_Tests_document"
"Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *)
TestKit
begin
section\<open>Test Purpose.\<close>
text\<open> Creation of document parts that are controlled by (nested, locally defined) monitors. \<close>
open_monitor*[aaa::Conceptual.M]
text*[test::A]\<open>For Test and Validation\<close>
text\<open>Defining some document elements to be referenced in later on in another theory: \<close>
text*[sdf] \<open> Lorem ipsum ... \<close> \<comment> \<open>anonymous reference, ignored by monitor.\<close>
text*[sdfg :: F] \<open> Lorem ipsum ...\<close> \<comment> \<open>causes just warnings for invariant violations
due to non-strict checking mode\<close>
close_monitor*[aaa] \<comment> \<open>causes warning: accept clause 1
not in final state .\<close>
section\<open>A Local Monitor Class Definition\<close>
doc_class test_monitor_free =
tmhd :: int
doc_class test_monitor_head =
tmhd :: int
doc_class test_monitor_A = test_monitor_head +
tmA :: int
doc_class test_monitor_B = test_monitor_A +
tmB :: int
doc_class test_monitor_C = test_monitor_A +
tmC :: int
doc_class test_monitor_D = test_monitor_B +
tmD :: int
doc_class test_monitor_E = test_monitor_D +
tmE :: int
doc_class monitor_M =
tmM :: int
rejects "test_monitor_A"
accepts "test_monitor_head ~~ test_monitor_B ~~ test_monitor_C"
section\<open>A more Complex Monitoring Example \<close>
text\<open>Consult the status of the DOF engine:\<close>
print_doc_classes
print_doc_items
declare[[free_class_in_monitor_checking]]
open_monitor*[test_monitor_M::monitor_M]
text*[testFree::test_monitor_free]\<open>...\<close>
open_monitor*[test_monitor_M2::monitor_M]
declare[[strict_monitor_checking]]
text-assert-error[test_monitor_A1::test_monitor_A]\<open>\<close>
\<open>accepts clause 1 of monitor Concept_MonitorTest1.test_monitor_M rejected\<close>
declare[[strict_monitor_checking=false]]
text*[test_monitor_A1::test_monitor_A]\<open>\<close> \<comment> \<open>the same in non-strict monitor checking.\<close>
declare[[free_class_in_monitor_strict_checking]]
text-assert-error[testFree2::test_monitor_free]\<open>\<close>
\<open>accepts clause 1 of monitor Concept_MonitorTest1.test_monitor_M not enabled\<close>
declare[[free_class_in_monitor_strict_checking=false]]
text*[test_monitor_head1::test_monitor_head]\<open>\<close>
text*[testFree3::test_monitor_free]\<open>\<close>
text*[test_monitor_B1::test_monitor_B]\<open>\<close>
text*[testFree4::test_monitor_free]\<open>\<close>
text*[test_monitor_D1::test_monitor_D]\<open>\<close>
text*[testFree5::test_monitor_free]\<open>\<close>
text*[test_monitor_C1::test_monitor_C]\<open>\<close>
text*[testFree6::test_monitor_free]\<open>\<close>
close_monitor*[test_monitor_M2]
close_monitor*[test_monitor_M]
declare[[free_class_in_monitor_checking = false]]
text\<open>Consult the final status of the DOF engine:\<close>
print_doc_classes
print_doc_items
ML\<open>
val (oid, DOF_core.Instance {value, ...}) =
Name_Space.check (Context.Proof \<^context>) (DOF_core.get_instances \<^context>) ("aaa", Position.none)
\<close>
term*\<open>map fst @{trace_attribute \<open>test_monitor_M\<close>}\<close>
value*\<open>map fst @{trace_attribute \<open>test_monitor_M\<close>}\<close>
ML\<open>@{assert} ([("Conceptual.A", "test"), ("Conceptual.F", "sdfg")] = @{trace_attribute aaa}) \<close>
open_monitor*[test_monitor_M3::monitor_M]
declare[[strict_monitor_checking]]
text-assert-error[test_monitor_A2::test_monitor_A]\<open>\<close>
\<open>accepts clause 1 of monitor Concept_MonitorTest1.test_monitor_M3 rejected\<close>
declare[[strict_monitor_checking=false]]
text*[test_monitor_A3::test_monitor_A]\<open>\<close> \<comment> \<open>the same in non-strict monitor checking.\<close>
declare[[free_class_in_monitor_strict_checking]]
text-assert-error[testFree7::test_monitor_free]\<open>\<close>
\<open>accepts clause 1 of monitor Concept_MonitorTest1.test_monitor_M3 not enabled\<close>
declare[[free_class_in_monitor_strict_checking=false]]
end