From 73dfcd6c1ecc603507d7aab1e9f71b633a65b9c8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Wed, 14 Dec 2022 12:02:15 +0100 Subject: [PATCH] Implement rejects clause MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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. --- .../Isabelle_DOF-Manual/04_RefMan.thy | 22 +- src/DOF/Isa_DOF.thy | 199 +++++++++++------- src/ontologies/Conceptual/Conceptual.thy | 45 +++- src/tests/Attributes.thy | 57 ++++- 4 files changed, 243 insertions(+), 80 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 170bddb..54c271d 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -1112,7 +1112,8 @@ text\ @{boxed_theory_text [display]\ declare[[invariants_checking_with_tactics = true]]\} There are still some limitations with this high-level syntax. - For now, the high-level syntax does not support monitors (see \<^technical>\sec:monitors\). + For now, the high-level syntax does not support the checking of + specific monitor behaviors (see \<^technical>\sec:monitors\). 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>\sec:low_level_inv\). @@ -1154,6 +1155,20 @@ text\ instances of \S\. \ text\ + 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>\strict_monitor_checking\ theory attribute: + @{boxed_theory_text [display]\declare[[strict_monitor_checking = true]]\} + It is possible to enable the tracing of free classes occurring inside the scope of a monitor by + enabling the \<^boxed_theory_text>\free_class_in_monitor_checking\ + theory attribute: + @{boxed_theory_text [display]\declare[[free_class_in_monitor_checking = true]]\} + 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>\free_class_in_monitor_strict_checking\ theory attribute: + @{boxed_theory_text [display]\declare[[free_class_in_monitor_strict_checking = true]]\} + 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>\example\ section by its own @@ -1171,8 +1186,9 @@ text\ 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>\sec:low_level_inv\.\ + 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>\sec:low_level_inv\).\ subsection*["sec:low_level_inv"::technical]\ODL Low-level Class Invariants\ diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index d4a8a09..c9693a5 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -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>\strict_monitor_checking\ (K false); +val (free_class_in_monitor_checking, free_class_in_monitor_checking_setup) + = Attrib.config_bool \<^binding>\free_class_in_monitor_checking\ (K false); + +val (free_class_in_monitor_strict_checking, free_class_in_monitor_strict_checking_setup) + = Attrib.config_bool \<^binding>\free_class_in_monitor_strict_checking\ (K false); + val (invariants_strict_checking, invariants_strict_checking_setup) = Attrib.config_bool \<^binding>\invariants_strict_checking\ (K false); @@ -825,6 +833,8 @@ end (* struct *) \ setup\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\ @@ -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 diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy index ff9631e..da79817 100644 --- a/src/ontologies/Conceptual/Conceptual.thy +++ b/src/ontologies/Conceptual/Conceptual.thy @@ -177,4 +177,47 @@ text*[ sdfg :: F] \ Lorem ipsum @{thm refl}\ text*[ xxxy ] \ Lorem ipsum @{F \sdfg\} rate @{thm refl}\ 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_monitor*[test_monitor_M2::monitor_M] + +text*[test_monitor_A1::test_monitor_A]\\ +text*[testFree2::test_monitor_free]\\ +text*[test_monitor_head1::test_monitor_head]\\ +text*[testFree3::test_monitor_free]\\ +text*[test_monitor_B1::test_monitor_B]\\ +text*[testFree4::test_monitor_free]\\ +text*[test_monitor_D1::test_monitor_D]\\ +text*[testFree5::test_monitor_free]\\ +text*[test_monitor_C1::test_monitor_C]\\ +text*[testFree6::test_monitor_free]\\ + +close_monitor*[test_monitor_M2] + +close_monitor*[test_monitor_M] + +end diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy index 3467795..762bccf 100644 --- a/src/tests/Attributes.thy +++ b/src/tests/Attributes.thy @@ -173,9 +173,20 @@ text\ @{docitem_attribute y::omega} \ section\Simulation of a Monitor\ +declare[[free_class_in_monitor_checking]] + +ML\ +val thy = \<^theory> +val long_cid = "Isa_COL.figure_group" +val t = DOF_core.get_doc_class_global long_cid thy +\ open_monitor*[figs1::figure_group, caption="''Sample ''"] - +ML\ +val thy = \<^theory> +val {monitor_tab,...} = DOF_core.get_data_global thy +\ +text*[testFreeA::A]\\ 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''"] \ The B train \ldots \ +open_monitor*[figs2::figure_group, + caption="''Sample ''"] +ML\ +val thy = \<^theory> +val {monitor_tab,...} = DOF_core.get_data_global thy +\ +figure*[fig_C::figure, spawn_columns=False, + relative_width="90", + src="''figures/A.png''"] + \ The C train \ldots \ +open_monitor*[figs3::figure_group, + caption="''Sample ''"] +ML\ +val thy = \<^theory> +val {monitor_tab,...} = DOF_core.get_data_global thy +\ + +figure*[fig_D::figure, + spawn_columns=False,relative_width="90", + src="''figures/B.png''"] + \ The D train \ldots \ +close_monitor*[figs3] + +open_monitor*[figs4::figure_group, + caption="''Sample ''"] +ML\ +val thy = \<^theory> +val {monitor_tab,...} = DOF_core.get_data_global thy +\ + +text*[testRejected1::figure_group, caption="''figures/A.png''"] + \ The A train \ldots \ + +figure*[fig_E::figure, + spawn_columns=False,relative_width="90", + src="''figures/B.png''"] + \ The E train \ldots \ +close_monitor*[figs4] +close_monitor*[figs2] +text*[testRejected2::figure_group, caption="''figures/A.png''"] + \ The A train \ldots \ close_monitor*[figs1] @@ -199,7 +251,8 @@ term*\map snd @{trace-attribute \figs1\}\ value*\map snd @{trace-attribute \figs1\}\ term*\map fst @{trace-attribute \aaa\}\ value*\map fst @{trace-attribute \aaa\}\ -value*\(map fst @{trace-attribute \aaa\}) \ +term*\map fst @{trace-attribute \test_monitor_M\}\ +value*\map fst @{trace-attribute \test_monitor_M\}\ definition example_expression where "example_expression \ \\''Conceptual.A''\ || \''Conceptual.F''\\\<^sup>*" value* \ DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \aaa\}) \