Add monitor tests

- Add tests for monitors spanning two theories.
- Fix monitors trace update bug.
  When updating a monitor trace when we define a new instance,
  the monitor instance is already defined.
  But we can not update the instance using the update_instance function
  because  this function needs a binding, i.e. a short name,
  and then it will update or define a new instance if we want
  to update a monitor in a super theory whose name is the same as
  a monitor defined in the current theory.
  Example:

  in the super theory:

  doc_class monitor_M =
  tmM :: int
  rejects "test_monitor_A"
  accepts "test_monitor_head ~~ test_monitor_B ~~ test_monitor_C"

  open_monitor*[test_monitor_M::monitor_M]

  in the current theory:

  doc_class monitor_M =
  tmM :: int
  rejects "test_monitor_B"
  accepts "test_monitor_E ~~ test_monitor_C"

  text*[test_monitor_head2::Concept_MonitorTest1.test_monitor_head]‹›
  open_monitor*[test_monitor_M3::monitor_M]
  ...
  ==> ERROR : the instantiation of test_monitor_head2
              will define a new instance current.test_monitor_M3
              when updating the trace of super.test_monitor_M3

  Hence we use the update_instance_entry function
  which uses long names and only updates the entry.

Isabelle_DOF-Unit-Tests/Concept_MonitorTest1.thy

@@ -77,8 +77,10 @@ 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>
-
-text*[testFree2::test_monitor_free]\<open>\<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>
@@ -107,5 +109,19 @@ 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 
   

Isabelle_DOF-Unit-Tests/Concept_MonitorTest2.thy

@@ -0,0 +1,65 @@
+(*************************************************************************
+ * 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_MonitorTest2
+  imports
+  Concept_MonitorTest1
+begin
+
+section\<open>Test Purpose.\<close>
+text\<open> Creation of document parts that are controlled by (nested, locally defined) monitors. \<close>
+
+doc_class monitor_M =
+  tmM :: int
+  rejects "test_monitor_B"
+  accepts "test_monitor_E ~~ test_monitor_C"
+
+doc_class test_monitor_head =
+  tmhd :: int
+
+declare[[free_class_in_monitor_checking]]
+
+declare[[free_class_in_monitor_strict_checking]]
+text-assert-error[test_monitor_head1::test_monitor_head]\<open>\<close>
+                  \<open>accepts clause 1 of monitor Concept_MonitorTest1.test_monitor_M3 not enabled\<close>
+declare[[free_class_in_monitor_strict_checking=false]]
+text*[test_monitor_head2::Concept_MonitorTest1.test_monitor_head]\<open>\<close>
+
+open_monitor*[test_monitor_M3::monitor_M]
+
+text*[test_monitor_head3::Concept_MonitorTest1.test_monitor_head]\<open>\<close>
+text*[testFree3::test_monitor_free]\<open>\<close>
+declare[[strict_monitor_checking]]
+text-assert-error[test_monitor_B1::test_monitor_B]\<open>\<close>
+                  \<open>accepts clause 1 of monitor Concept_MonitorTest2.test_monitor_M3 rejected\<close>
+declare[[strict_monitor_checking=false]]
+text*[testFree4::test_monitor_free]\<open>\<close>
+declare[[strict_monitor_checking]]
+text-assert-error[test_monitor_D1::test_monitor_D]\<open>\<close>
+                  \<open>accepts clause 1 of monitor Concept_MonitorTest2.test_monitor_M3 rejected\<close>
+declare[[strict_monitor_checking=false]]
+text*[testFree5::test_monitor_free]\<open>\<close>
+text*[test_monitor_E1::test_monitor_E]\<open>\<close>
+text*[test_monitor_C1::test_monitor_C]\<open>\<close>
+text*[testFree6::test_monitor_free]\<open>\<close>
+
+close_monitor*[Concept_MonitorTest1.test_monitor_M3]
+
+close_monitor*[test_monitor_M3]
+
+declare[[free_class_in_monitor_checking = false]]
+
+end

Isabelle_DOF-Unit-Tests/ROOT

@@ -7,6 +7,7 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
     "Concept_Example_Low_Level_Invariant"
     "Concept_High_Level_Invariants"
     "Concept_MonitorTest1"
+    "Concept_MonitorTest2"
     "Concept_TermAntiquotations"
     "Attributes"
     "Evaluation"

Isabelle_DOF/thys/Isa_DOF.thy

@@ -262,6 +262,8 @@ struct
      cid: string,
      vcid: string option}
 
+  val undefined_instance = "undefined_instance"
+
   val empty_instance = Instance {defined = false,
      input_term = \<^term>\<open>()\<close>,
      value = \<^term>\<open>()\<close>,
@@ -626,20 +628,26 @@ fun define_object_global {define = define} ((oid, pos), instance) thy  =
     val binding = if Long_Name.is_qualified oid
                   then Binding.make (Long_Name.base_name oid, pos)
                   else Binding.make (oid, pos)
-    val undefined_instance = "undefined_instance"
+    val _ = if oid = undefined_instance
+            then error (oid ^ ": This name is reserved by the implementation" ^ Position.here pos)
+            else ()
     val (oid', instance') = Name_Space.check (Context.Theory thy)
                                 (get_instances (Proof_Context.init_global thy)) (oid, Position.none)
                                 handle ERROR _ => (undefined_instance, empty_instance)
     val Instance {input_term, value, inline, cid, vcid, ...} = instance
     val instance'' = make_instance (define, input_term, value, inline, cid, vcid)
   in if oid' = undefined_instance andalso instance' = empty_instance
-     then add_instance binding instance'' thy
-     else if define 
+     then (* declare instance using declare_reference* or else define instance *)
+          add_instance binding instance'' thy
+     else if define
           then let val Instance {defined, ...} = instance'
                in  if defined
-                   then add_instance binding instance'' thy
-                   else update_instance_entry oid' instance'' thy end
-          else add_instance binding instance thy
+                   then (* trigger error when adding already defined instance *)
+                        add_instance binding instance'' thy
+                   else (* define already declared instance *)
+                        update_instance_entry oid' instance'' thy end
+          else (* trigger error with declare_reference* when declaring already declared instance *)
+               add_instance binding instance thy
   end
 
 
@@ -725,17 +733,17 @@ fun binding_from_instance_pos name thy  =
 
 fun update_value_global name upd_value thy  =
   let
-    val binding = binding_from_instance_pos name thy
+    val name' = get_instance_name_global name thy
     val Instance {defined, input_term, value, inline, cid, vcid} = get_instance_global name thy 
     val instance' = make_instance (defined, input_term, upd_value value, inline, cid, vcid)
-  in update_instance binding instance' thy end
+  in update_instance_entry name' instance' thy end
 
 fun update_input_term_global name upd_input_term thy  = 
   let
-    val binding = binding_from_instance_pos name thy
+    val name' = get_instance_name_global name thy
     val Instance {defined, input_term, value, inline, cid, vcid} = get_instance_global name thy 
     val instance' = make_instance (defined, upd_input_term input_term, value, inline, cid, vcid)
-  in update_instance binding instance' thy end
+  in update_instance_entry name' instance' thy end
 
 fun update_value_input_term_global name upd_input_term upd_value thy  = 
   update_value_global name upd_value thy |> update_input_term_global name upd_input_term