Implement rejects clause
ci/woodpecker/push/build Pipeline was successful
Details
ci/woodpecker/push/build Pipeline was successful
Details
- The current implementation triggers a warning when
rejected classes are find in the monitor,
and an error if monitor_strict_checking is enable.
It follows these rules:
Inside the scope of a monitor,
all instances of classes mentioned in its accepts_clause
(the ∗‹accept-set›) have to appear in the order specified
by the regular expression.
Instances not covered by an accept-set may freely occur.
Monitors may additionally contain a rejects_clause
with a list of class-ids (the reject-list).
This allows specifying ranges of
admissible instances along the class hierarchy:
- a superclass in the reject-list and a subclass in the
accept-expression forbids instances superior to the subclass, and
- a subclass S in the reject-list and a superclass T in the
accept-list allows instances of superclasses of T to occur freely,
instances of T to occur in the specified order and forbids
instances of S.
- No message is triggered for the free classes,
but two theory options, free_class_in_monitor_checking
and free_class_in_monitor_strict_checking,
are added and can be used if we want to trigger warnings or errors,
in the case we do not want free classes inside a monitor.
- Fix the checking warning when defining a monitor,
as the monitor was added to the monitor table and then
the instance of the monitor was added to the theory.
So a monitor had the bad behavior to check itself.
This commit is contained in:
Nicolas Méric
parent
c0afe1105e
commit
73dfcd6c1e
|
|
@ -1112,7 +1112,8 @@ text\<open>
|
|||
@{boxed_theory_text [display]\<open>
|
||||
declare[[invariants_checking_with_tactics = true]]\<close>}
|
||||
There are still some limitations with this high-level syntax.
|
||||
For now, the high-level syntax does not support monitors (see \<^technical>\<open>sec:monitors\<close>).
|
||||
For now, the high-level syntax does not support the checking of
|
||||
specific monitor behaviors (see \<^technical>\<open>sec:monitors\<close>).
|
||||
For example, one would like to delay a final error message till the
|
||||
closing of a monitor.
|
||||
For this use-case you can use low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>).
|
||||
|
|
@ -1154,6 +1155,20 @@ text\<open>
|
|||
instances of \<open>S\<close>.
|
||||
\<close>
|
||||
text\<open>
|
||||
Should the specified ranges of admissible instances not be observed, warnings will be triggered.
|
||||
To forbid the violation of the specified ranges,
|
||||
one can enable the \<^boxed_theory_text>\<open>strict_monitor_checking\<close> theory attribute:
|
||||
@{boxed_theory_text [display]\<open>declare[[strict_monitor_checking = true]]\<close>}
|
||||
It is possible to enable the tracing of free classes occurring inside the scope of a monitor by
|
||||
enabling the \<^boxed_theory_text>\<open>free_class_in_monitor_checking\<close>
|
||||
theory attribute:
|
||||
@{boxed_theory_text [display]\<open>declare[[free_class_in_monitor_checking = true]]\<close>}
|
||||
Then a warning will be triggered when defining an instance of a free class
|
||||
inside the scope of a monitor.
|
||||
To forbid free classes inside the scope of a monitor, one can enable the
|
||||
\<^boxed_theory_text>\<open>free_class_in_monitor_strict_checking\<close> theory attribute:
|
||||
@{boxed_theory_text [display]\<open>declare[[free_class_in_monitor_strict_checking = true]]\<close>}
|
||||
|
||||
Monitored document sections can be nested and overlap; thus, it is
|
||||
possible to combine the effect of different monitors. For example, it
|
||||
would be possible to refine the \<^boxed_theory_text>\<open>example\<close> section by its own
|
||||
|
|
@ -1171,8 +1186,9 @@ text\<open>
|
|||
header delimiting the borders of its representation. Class invariants
|
||||
on monitors allow for specifying structural properties on document
|
||||
sections.
|
||||
For now, the high-level syntax of invariants is not supported for monitors and you must use
|
||||
the low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>.\<close>
|
||||
For now, the high-level syntax of invariants does not support the checking of
|
||||
specific monitor behaviors like the one above and you must use
|
||||
the low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>).\<close>
|
||||
|
||||
|
||||
subsection*["sec:low_level_inv"::technical]\<open>ODL Low-level Class Invariants\<close>
|
||||
|
|
|
|||
|
|
@ -346,6 +346,8 @@ fun upd_docclass_lazy_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab,
|
|||
docclass_lazy_inv_tab=f docclass_lazy_inv_tab};
|
||||
|
||||
fun get_accepted_cids ({accepted_cids, ... } : open_monitor_info) = accepted_cids
|
||||
fun get_rejected_cids ({rejected_cids, ... } : open_monitor_info) = rejected_cids
|
||||
fun get_alphabet monitor_info = (get_accepted_cids monitor_info) @ (get_rejected_cids monitor_info)
|
||||
fun get_automatas ({automatas, ... } : open_monitor_info) = automatas
|
||||
|
||||
|
||||
|
|
@ -813,6 +815,12 @@ fun print_doc_class_tree ctxt P T =
|
|||
val (strict_monitor_checking, strict_monitor_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
|
||||
|
||||
val (free_class_in_monitor_checking, free_class_in_monitor_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>free_class_in_monitor_checking\<close> (K false);
|
||||
|
||||
val (free_class_in_monitor_strict_checking, free_class_in_monitor_strict_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>free_class_in_monitor_strict_checking\<close> (K false);
|
||||
|
||||
val (invariants_strict_checking, invariants_strict_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>invariants_strict_checking\<close> (K false);
|
||||
|
||||
|
|
@ -825,6 +833,8 @@ end (* struct *)
|
|||
\<close>
|
||||
|
||||
setup\<open>DOF_core.strict_monitor_checking_setup
|
||||
#> DOF_core.free_class_in_monitor_checking_setup
|
||||
#> DOF_core.free_class_in_monitor_strict_checking_setup
|
||||
#> DOF_core.invariants_strict_checking_setup
|
||||
#> DOF_core.invariants_checking_with_tactics_setup\<close>
|
||||
|
||||
|
|
@ -1434,7 +1444,7 @@ fun create_default_object thy class_name =
|
|||
in list_comb (make_const, (tag_attr (serial()))::class_list'') end
|
||||
|
||||
|
||||
fun check_classref {is_monitor=is_monitor} (SOME(cid,pos')) thy =
|
||||
fun check_classref {is_monitor=is_monitor} (SOME(cid,pos)) thy =
|
||||
let
|
||||
val cid_long = DOF_core.read_cid_global thy cid
|
||||
|
||||
|
|
@ -1444,10 +1454,10 @@ fun check_classref {is_monitor=is_monitor} (SOME(cid,pos')) thy =
|
|||
else ()
|
||||
val markup = docclass_markup false cid id (Binding.pos_of bind_target);
|
||||
val ctxt = Context.Theory thy
|
||||
val _ = Context_Position.report_generic ctxt pos' markup;
|
||||
in cid_long
|
||||
val _ = Context_Position.report_generic ctxt pos markup;
|
||||
in (cid_long, pos)
|
||||
end
|
||||
| check_classref _ NONE _ = DOF_core.default_cid
|
||||
| check_classref _ NONE _ = (DOF_core.default_cid, \<^here>)
|
||||
|
||||
|
||||
fun generalize_typ n = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,n),sort));
|
||||
|
|
@ -1515,67 +1525,104 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long
|
|||
end
|
||||
in Sign.certify_term thy (fold read_assn S term) end
|
||||
|
||||
fun msg thy txt = if Config.get_global thy DOF_core.strict_monitor_checking
|
||||
then error txt
|
||||
else warning txt
|
||||
fun msg thy txt pos = if Config.get_global thy DOF_core.strict_monitor_checking
|
||||
then ISA_core.err txt pos
|
||||
else ISA_core.warn txt pos
|
||||
|
||||
fun register_oid_cid_in_open_monitors oid pos cid_long thy =
|
||||
let val {monitor_tab,...} = DOF_core.get_data_global thy
|
||||
fun is_enabled (n, info) =
|
||||
if exists (DOF_core.is_subclass_global thy cid_long)
|
||||
(DOF_core.get_accepted_cids info)
|
||||
then SOME n
|
||||
else NONE
|
||||
(* filtering those monitors with automata, whose alphabet contains the
|
||||
cid of this oid. The enabled ones were selected and moved to their successor state
|
||||
along the super-class id. The evaluation is in parallel, simulating a product
|
||||
semantics without expanding the subclass relationship. *)
|
||||
fun is_enabled_for_cid moid =
|
||||
let val {accepted_cids, automatas, ...} =
|
||||
the(Symtab.lookup monitor_tab moid)
|
||||
val indexS= 1 upto (length automatas)
|
||||
val indexed_autoS = automatas ~~ indexS
|
||||
fun check_for_cid (A,n) =
|
||||
let val accS = (RegExpInterface.enabled A accepted_cids)
|
||||
val is_subclass = DOF_core.is_subclass_global thy
|
||||
val idx = find_index (is_subclass cid_long) accS
|
||||
in if idx < 0
|
||||
then (msg thy ("monitor "^moid^"(" ^ Int.toString n
|
||||
^") not enabled for doc_class: "^cid_long);A)
|
||||
else RegExpInterface.next A accepted_cids (nth accS idx)
|
||||
fun register_oid_cid_in_open_monitors oid pos cid_pos thy =
|
||||
let val {monitor_tab,...} = DOF_core.get_data_global thy
|
||||
val cid_long= fst cid_pos
|
||||
val pos' = snd cid_pos
|
||||
fun is_enabled (n, info) =
|
||||
if exists (DOF_core.is_subclass_global thy cid_long)
|
||||
(DOF_core.get_alphabet info)
|
||||
then SOME n
|
||||
else if Config.get_global thy DOF_core.free_class_in_monitor_strict_checking
|
||||
orelse Config.get_global thy DOF_core.free_class_in_monitor_checking
|
||||
then SOME n
|
||||
else NONE
|
||||
(* filtering those monitors with automata, whose alphabet contains the
|
||||
cid of this oid. The enabled ones were selected and moved to their successor state
|
||||
along the super-class id. The evaluation is in parallel, simulating a product
|
||||
semantics without expanding the subclass relationship. *)
|
||||
fun is_enabled_for_cid moid =
|
||||
let val {accepted_cids, automatas, rejected_cids, ...} =
|
||||
the(Symtab.lookup monitor_tab moid)
|
||||
val indexS= 1 upto (length automatas)
|
||||
val indexed_autoS = automatas ~~ indexS
|
||||
fun check_for_cid (A,n) =
|
||||
let fun direct_super_class _ cid [] = cid
|
||||
| direct_super_class thy cid (x::xs) =
|
||||
if DOF_core.is_subclass_global thy cid x
|
||||
then direct_super_class thy cid xs
|
||||
else direct_super_class thy x xs
|
||||
val accS = (RegExpInterface.enabled A accepted_cids)
|
||||
val accS' = filter (DOF_core.is_subclass_global thy cid_long) accS
|
||||
fun first_super_class cids =
|
||||
case List.getItem cids
|
||||
of SOME (hd,tl) => SOME (direct_super_class thy hd tl)
|
||||
| NONE => NONE
|
||||
val first_accepted = first_super_class accS'
|
||||
val rejectS = filter (DOF_core.is_subclass_global thy cid_long) rejected_cids
|
||||
val first_rejected = first_super_class rejectS
|
||||
in
|
||||
case first_accepted of
|
||||
NONE => (case first_rejected of
|
||||
NONE =>
|
||||
let val msg_intro = ("accepts clause " ^ Int.toString n
|
||||
^ " of monitor " ^ moid
|
||||
^ " not enabled for doc_class: " ^ cid_long)
|
||||
in
|
||||
if Config.get_global thy DOF_core.free_class_in_monitor_strict_checking
|
||||
then ISA_core.err msg_intro pos'
|
||||
else if Config.get_global thy DOF_core.free_class_in_monitor_checking
|
||||
then (ISA_core.warn msg_intro pos';A)
|
||||
else A
|
||||
end
|
||||
in (moid,map check_for_cid indexed_autoS) end
|
||||
val enabled_monitors = List.mapPartial is_enabled (Symtab.dest monitor_tab)
|
||||
fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn,
|
||||
Syntax.read_term_global thy rhs)
|
||||
val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")]
|
||||
val assns' = map conv_attrs trace_attr
|
||||
fun cid_of oid = #cid(the(DOF_core.get_object_global oid thy))
|
||||
fun def_trans_input_term oid =
|
||||
#1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns')
|
||||
fun def_trans_value oid =
|
||||
(#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns'))
|
||||
#> value (Proof_Context.init_global thy)
|
||||
val _ = if null enabled_monitors then () else writeln "registrating in monitors ..."
|
||||
val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors;
|
||||
(* check that any transition is possible : *)
|
||||
fun inst_class_inv x = DOF_core.get_class_invariant(cid_of x) thy x {is_monitor=false}
|
||||
fun class_inv_checks ctxt = map (fn x => inst_class_inv x ctxt) enabled_monitors
|
||||
val delta_autoS = map is_enabled_for_cid enabled_monitors;
|
||||
fun update_info (n, aS) (tab: DOF_core.monitor_tab) =
|
||||
let val {accepted_cids,rejected_cids,...} = the(Symtab.lookup tab n)
|
||||
in Symtab.update(n, {accepted_cids=accepted_cids,
|
||||
rejected_cids=rejected_cids,
|
||||
automatas=aS}) tab end
|
||||
fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans_input_term mon_oid) (def_trans_value mon_oid)
|
||||
val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS)
|
||||
in thy |> (* update traces of all enabled monitors *)
|
||||
fold (update_trace) (enabled_monitors)
|
||||
|> (* check class invariants of enabled monitors *)
|
||||
(fn thy => (class_inv_checks (Context.Theory thy); thy))
|
||||
|> (* update the automata of enabled monitors *)
|
||||
DOF_core.map_data_global(update_automatons)
|
||||
end
|
||||
| SOME _ => (msg thy ("accepts clause " ^ Int.toString n
|
||||
^ " of monitor " ^ moid
|
||||
^ " rejected doc_class: " ^ cid_long) pos';A))
|
||||
| SOME accepted => (case first_rejected of
|
||||
NONE => RegExpInterface.next A accepted_cids (accepted)
|
||||
| SOME rejected =>
|
||||
if DOF_core.is_subclass_global thy accepted rejected
|
||||
then RegExpInterface.next A accepted_cids (accepted)
|
||||
else (msg thy ("accepts clause " ^ Int.toString n
|
||||
^ " of monitor " ^ moid
|
||||
^ " rejected doc_class: " ^ cid_long) pos';A))
|
||||
end
|
||||
in (moid,map check_for_cid indexed_autoS) end
|
||||
val enabled_monitors = List.mapPartial is_enabled (Symtab.dest monitor_tab)
|
||||
fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn,
|
||||
Syntax.read_term_global thy rhs)
|
||||
val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")]
|
||||
val assns' = map conv_attrs trace_attr
|
||||
fun cid_of oid = #cid(the(DOF_core.get_object_global oid thy))
|
||||
fun def_trans_input_term oid =
|
||||
#1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns')
|
||||
fun def_trans_value oid =
|
||||
(#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns'))
|
||||
#> value (Proof_Context.init_global thy)
|
||||
val _ = if null enabled_monitors then () else writeln "registrating in monitors ..."
|
||||
val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors;
|
||||
(* check that any transition is possible : *)
|
||||
fun inst_class_inv x = DOF_core.get_class_invariant(cid_of x) thy x {is_monitor=false}
|
||||
fun class_inv_checks ctxt = map (fn x => inst_class_inv x ctxt) enabled_monitors
|
||||
val delta_autoS = map is_enabled_for_cid enabled_monitors;
|
||||
fun update_info (n, aS) (tab: DOF_core.monitor_tab) =
|
||||
let val {accepted_cids,rejected_cids,...} = the(Symtab.lookup tab n)
|
||||
in Symtab.update(n, {accepted_cids=accepted_cids,
|
||||
rejected_cids=rejected_cids,
|
||||
automatas=aS}) tab end
|
||||
fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans_input_term mon_oid) (def_trans_value mon_oid)
|
||||
val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS)
|
||||
in thy |> (* update traces of all enabled monitors *)
|
||||
fold (update_trace) (enabled_monitors)
|
||||
|> (* check class invariants of enabled monitors *)
|
||||
(fn thy => (class_inv_checks (Context.Theory thy); thy))
|
||||
|> (* update the automata of enabled monitors *)
|
||||
DOF_core.map_data_global(update_automatons)
|
||||
end
|
||||
|
||||
fun check_invariants thy oid =
|
||||
let
|
||||
|
|
@ -1655,7 +1702,8 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
|
|||
val _ = Position.report pos (docref_markup true oid id pos);
|
||||
(* creates a markup label for this position and reports it to the PIDE framework;
|
||||
this label is used as jump-target for point-and-click feature. *)
|
||||
val cid_long = check_classref is_monitor cid_pos thy
|
||||
val cid_pos' = check_classref is_monitor cid_pos thy
|
||||
val cid_long = fst cid_pos'
|
||||
val default_cid = cid_long = DOF_core.default_cid
|
||||
val vcid = case cid_pos of NONE => NONE
|
||||
| SOME (cid,_) => if (DOF_core.is_virtual cid thy)
|
||||
|
|
@ -1694,7 +1742,7 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
|
|||
id = id,
|
||||
cid = cid_long,
|
||||
vcid = vcid})
|
||||
|> register_oid_cid_in_open_monitors oid pos cid_long
|
||||
|> register_oid_cid_in_open_monitors oid pos cid_pos'
|
||||
|> (fn thy => if #is_monitor(is_monitor)
|
||||
then (((DOF_core.get_class_eager_invariant cid_long thy oid) is_monitor
|
||||
o Context.Theory) thy; thy)
|
||||
|
|
@ -1870,8 +1918,9 @@ fun update_instance_command (((oid:string,pos),cid_pos),
|
|||
val _ = Context_Position.report ctxt pos markup;
|
||||
in cid end
|
||||
| NONE => error("undefined doc_class.")
|
||||
val cid_long = Value_Command.Docitem_Parser.check_classref {is_monitor = false}
|
||||
val cid_pos' = Value_Command.Docitem_Parser.check_classref {is_monitor = false}
|
||||
cid_pos thy
|
||||
val cid_long = fst cid_pos'
|
||||
val _ = if cid_long = DOF_core.default_cid orelse cid = cid_long
|
||||
then ()
|
||||
else error("incompatible classes:"^cid^":"^cid_long)
|
||||
|
|
@ -1911,31 +1960,33 @@ fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Pars
|
|||
in
|
||||
case DOF_core.get_doc_class_global long_cid thy of
|
||||
SOME X => let val ralph = RegExpInterface.alphabet (#rejectS X)
|
||||
val alph = RegExpInterface.ext_alphabet ralph (#rex X)
|
||||
in (alph, map (RegExpInterface.rexp_term2da alph)(#rex X)) end
|
||||
val aalph = RegExpInterface.alphabet (#rex X)
|
||||
in (aalph, ralph, map (RegExpInterface.rexp_term2da aalph)(#rex X)) end
|
||||
| NONE => error("Internal error: class id undefined. ")
|
||||
end
|
||||
fun create_monitor_entry thy =
|
||||
let val cid = case cid_pos of
|
||||
NONE => ISA_core.err ("You must specified a monitor class.") pos
|
||||
| SOME (cid, _) => cid
|
||||
val (S, aS) = compute_enabled_set cid thy
|
||||
val info = {accepted_cids = S, rejected_cids = [], automatas = aS }
|
||||
val (accS, rejectS, aS) = compute_enabled_set cid thy
|
||||
val info = {accepted_cids = accS, rejected_cids = rejectS, automatas = aS }
|
||||
in DOF_core.map_data_global(DOF_core.upd_monitor_tabs(Symtab.update(oid, info )))(thy)
|
||||
end
|
||||
in
|
||||
create_monitor_entry #> o_m_c oid pos cid_pos doc_attrs
|
||||
o_m_c oid pos cid_pos doc_attrs #> create_monitor_entry
|
||||
end;
|
||||
|
||||
|
||||
fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|
||||
doc_attrs: (((string*Position.T)*string)*string)list)) thy =
|
||||
let val {monitor_tab,...} = DOF_core.get_data_global thy
|
||||
fun check_if_final aS = let val i = find_index (not o RegExpInterface.final) aS
|
||||
in if i >= 0
|
||||
fun check_if_final aS = let val i = (find_index (not o RegExpInterface.final) aS) + 1
|
||||
in if i >= 1
|
||||
then
|
||||
Value_Command.Docitem_Parser.msg thy
|
||||
("monitor number "^Int.toString i^" not in final state.")
|
||||
("accepts clause " ^ Int.toString i
|
||||
^ " of monitor " ^ oid
|
||||
^ " not in final state.") pos
|
||||
else ()
|
||||
end
|
||||
val _ = case Symtab.lookup monitor_tab oid of
|
||||
|
|
|
|||
|
|
@ -177,4 +177,47 @@ text*[ sdfg :: F] \<open> Lorem ipsum @{thm refl}\<close>
|
|||
text*[ xxxy ] \<open> Lorem ipsum @{F \<open>sdfg\<close>} rate @{thm refl}\<close>
|
||||
close_monitor*[aaa]
|
||||
|
||||
end
|
||||
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"
|
||||
|
||||
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]
|
||||
|
||||
text*[test_monitor_A1::test_monitor_A]\<open>\<close>
|
||||
text*[testFree2::test_monitor_free]\<open>\<close>
|
||||
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]
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -173,9 +173,20 @@ text\<open> @{docitem_attribute y::omega} \<close>
|
|||
|
||||
section\<open>Simulation of a Monitor\<close>
|
||||
|
||||
declare[[free_class_in_monitor_checking]]
|
||||
|
||||
ML\<open>
|
||||
val thy = \<^theory>
|
||||
val long_cid = "Isa_COL.figure_group"
|
||||
val t = DOF_core.get_doc_class_global long_cid thy
|
||||
\<close>
|
||||
open_monitor*[figs1::figure_group,
|
||||
caption="''Sample ''"]
|
||||
|
||||
ML\<open>
|
||||
val thy = \<^theory>
|
||||
val {monitor_tab,...} = DOF_core.get_data_global thy
|
||||
\<close>
|
||||
text*[testFreeA::A]\<open>\<close>
|
||||
figure*[fig_A::figure, spawn_columns=False,
|
||||
relative_width="90",
|
||||
src="''figures/A.png''"]
|
||||
|
|
@ -185,6 +196,47 @@ figure*[fig_B::figure,
|
|||
spawn_columns=False,relative_width="90",
|
||||
src="''figures/B.png''"]
|
||||
\<open> The B train \ldots \<close>
|
||||
open_monitor*[figs2::figure_group,
|
||||
caption="''Sample ''"]
|
||||
ML\<open>
|
||||
val thy = \<^theory>
|
||||
val {monitor_tab,...} = DOF_core.get_data_global thy
|
||||
\<close>
|
||||
figure*[fig_C::figure, spawn_columns=False,
|
||||
relative_width="90",
|
||||
src="''figures/A.png''"]
|
||||
\<open> The C train \ldots \<close>
|
||||
open_monitor*[figs3::figure_group,
|
||||
caption="''Sample ''"]
|
||||
ML\<open>
|
||||
val thy = \<^theory>
|
||||
val {monitor_tab,...} = DOF_core.get_data_global thy
|
||||
\<close>
|
||||
|
||||
figure*[fig_D::figure,
|
||||
spawn_columns=False,relative_width="90",
|
||||
src="''figures/B.png''"]
|
||||
\<open> The D train \ldots \<close>
|
||||
close_monitor*[figs3]
|
||||
|
||||
open_monitor*[figs4::figure_group,
|
||||
caption="''Sample ''"]
|
||||
ML\<open>
|
||||
val thy = \<^theory>
|
||||
val {monitor_tab,...} = DOF_core.get_data_global thy
|
||||
\<close>
|
||||
|
||||
text*[testRejected1::figure_group, caption="''figures/A.png''"]
|
||||
\<open> The A train \ldots \<close>
|
||||
|
||||
figure*[fig_E::figure,
|
||||
spawn_columns=False,relative_width="90",
|
||||
src="''figures/B.png''"]
|
||||
\<open> The E train \ldots \<close>
|
||||
close_monitor*[figs4]
|
||||
close_monitor*[figs2]
|
||||
text*[testRejected2::figure_group, caption="''figures/A.png''"]
|
||||
\<open> The A train \ldots \<close>
|
||||
|
||||
close_monitor*[figs1]
|
||||
|
||||
|
|
@ -199,7 +251,8 @@ term*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
|
|||
value*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
|
||||
term*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
|
||||
value*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
|
||||
value*\<open>(map fst @{trace-attribute \<open>aaa\<close>}) \<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>
|
||||
|
||||
definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*"
|
||||
value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>
|
||||
|
|
|
|||
Loading…
Reference in New Issue