forked from Isabelle_DOF/Isabelle_DOF
parent
6a6adaab1e
commit
218ff9f7ec
|
@ -1530,6 +1530,8 @@ fun msg' thy txt = if Config.get_global thy DOF_core.free_class_in_monitor_stric
|
|||
|
||||
fun register_oid_cid_in_open_monitors {is_monitor=is_monitor} oid pos cid_long thy =
|
||||
let val {monitor_tab,...} = DOF_core.get_data_global thy
|
||||
val _ = writeln("In register_oid_cid_in_open_monitors oid: " ^ oid)
|
||||
val _ = writeln("In register_oid_cid_in_open_monitors cid_long: " ^ cid_long)
|
||||
fun is_enabled (n, info) =
|
||||
if exists (DOF_core.is_subclass_global thy cid_long)
|
||||
(DOF_core.get_alphabet info)
|
||||
|
@ -1559,6 +1561,11 @@ fun register_oid_cid_in_open_monitors {is_monitor=is_monitor} oid pos cid_long t
|
|||
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
|
||||
val _ = writeln("In is_enabled_for_cid accepted_cids: " ^ \<^make_string> accepted_cids)
|
||||
val _ = writeln("In is_enabled_for_cid accS: " ^ \<^make_string> accS)
|
||||
val _ = writeln("In is_enabled_for_cid accS': " ^ \<^make_string> accS')
|
||||
val _ = writeln("In is_enabled_for_cid rejected_cids: " ^ \<^make_string> rejected_cids)
|
||||
val _ = writeln("In is_enabled_for_cid rejectS: " ^ \<^make_string> rejectS)
|
||||
val _ = writeln("In is_enabled_for_cid cid_long: " ^ cid_long)
|
||||
val _ = writeln("In is_enabled_for_cid first_accepted: " ^ \<^make_string> first_accepted)
|
||||
val _ = writeln("In is_enabled_for_cid first_rejected: " ^ \<^make_string> first_rejected)
|
||||
|
@ -1579,6 +1586,7 @@ fun register_oid_cid_in_open_monitors {is_monitor=is_monitor} oid pos cid_long t
|
|||
end
|
||||
in (moid,map check_for_cid indexed_autoS) end
|
||||
val enabled_monitors = List.mapPartial is_enabled (Symtab.dest monitor_tab)
|
||||
val _ = writeln("In register_oid_cid_in_open_monitors enabled_monitors: " ^ \<^make_string> enabled_monitors)
|
||||
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^"'')]")]
|
||||
|
@ -1594,6 +1602,7 @@ fun register_oid_cid_in_open_monitors {is_monitor=is_monitor} oid pos cid_long t
|
|||
(* 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 _ = writeln("In register_oid_cid_in_open_monitors cid_long: " ^ cid_long)
|
||||
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)
|
||||
|
|
|
@ -173,9 +173,18 @@ text\<open> @{docitem_attribute y::omega} \<close>
|
|||
|
||||
section\<open>Simulation of a Monitor\<close>
|
||||
|
||||
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*[testA::A]\<open>\<close>
|
||||
figure*[fig_A::figure, spawn_columns=False,
|
||||
relative_width="90",
|
||||
src="''figures/A.png''"]
|
||||
|
@ -185,9 +194,46 @@ 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 A 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 B 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*[test2::figure_group, caption="''figures/A.png''"]
|
||||
\<open> The A train \ldots \<close>
|
||||
close_monitor*[figs4]
|
||||
close_monitor*[figs2]
|
||||
text*[test1::figure_group, caption="''figures/A.png''"]
|
||||
\<open> The A train \ldots \<close>
|
||||
|
||||
close_monitor*[figs1]
|
||||
|
||||
|
||||
text\<open>Resulting trace of figs1 as ML antiquotation: \<close>
|
||||
ML \<open>@{trace_attribute figs1}\<close>
|
||||
text\<open>Resulting trace of figs as text antiquotation:\<close>
|
||||
|
|
Loading…
Reference in New Issue