From 218ff9f7ecf4e3ff4cdda7a64bd4e7cd0109f6d2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Wed, 14 Dec 2022 14:36:19 +0100
Subject: [PATCH] Fix checking warning of monitors for monitors

WIP
---
 src/DOF/Isa_DOF.thy      |  9 ++++++++
 src/tests/Attributes.thy | 48 +++++++++++++++++++++++++++++++++++++++-
 2 files changed, 56 insertions(+), 1 deletion(-)

diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy
index 9160a635..ae19d2df 100644
--- a/src/DOF/Isa_DOF.thy
+++ b/src/DOF/Isa_DOF.thy
@@ -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)
diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy
index 3467795d..10efd491 100644
--- a/src/tests/Attributes.thy
+++ b/src/tests/Attributes.thy
@@ -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>