128 lines
4.8 KiB
Plaintext
128 lines
4.8 KiB
Plaintext
(*************************************************************************
|
|
* 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
|
|
|