diff --git a/Isa_DOF.thy b/Isa_DOF.thy index e632bafe..eed052ed 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -956,7 +956,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy = 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, rejected_cids, automatas} = + let val {accepted_cids, automatas, ...} = the(Symtab.lookup monitor_tab moid) val indexS= 1 upto (length automatas) val indexed_autoS = automatas ~~ indexS @@ -981,16 +981,22 @@ fun register_oid_cid_in_open_monitors oid pos cid_long 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,automatas} = the(Symtab.lookup tab n) + 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 mon_oid) val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) - in thy |> fold (update_trace) (enabled_monitors) - |> DOF_core.map_data_global(update_automatons) + 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 diff --git a/examples/conceptual/Concept_ExampleInvariant.thy b/examples/conceptual/Concept_ExampleInvariant.thy index 0a7bcaa0..114318e1 100644 --- a/examples/conceptual/Concept_ExampleInvariant.thy +++ b/examples/conceptual/Concept_ExampleInvariant.thy @@ -36,13 +36,11 @@ ML\fun check_A_invariant oid {is_monitor:bool} ctxt = setup\DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\ -(* test : should fail : *) -subsection*[c::A, x = "6"] \ Lorem ipsum dolor sit amet, ... \ -subsection*[d::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ +subsection*[d::A, x = "4"] \ Lorem ipsum dolor sit amet, ... \ -(* test : update should fail : *) +(* test : update should not fail, invariant still valid *) update_instance*[d::A, x += "1"] @@ -63,7 +61,7 @@ that instances of class C occur more often as those of class D; note that this i to take sub-classing into account: \ -ML\fun check_M_invariant oid {is_monitor} ctxt = +ML\fun check_M_invariant oid {is_monitor} ctxt = let val term = AttributeAccess.calc_attr_access ctxt "trace" oid @{here} fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) val string_pair_list = map conv (HOLogic.dest_list term) @@ -94,6 +92,7 @@ section*[f::E] \ Lectus accumsan velit ultrices, ... }\ Lectus accumsan velit ultrices, ... }\ *) + ML\val term = AttributeAccess.calc_attr_access (Context.Proof @{context}) "trace" "struct" @{here}; fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) val string_pair_list = map conv (HOLogic.dest_list term) diff --git a/test/cenelec/Example.thy b/test/cenelec/Example.thy index bdadced5..7efa37ef 100644 --- a/test/cenelec/Example.thy +++ b/test/cenelec/Example.thy @@ -97,8 +97,7 @@ text{* @{test_specification \ass122\} -- wrong: "reference ontologi text{* Here is a reference to @{docref \sedf\} *} -(* works currently only in connection with the above label-hack. - Try to hover over the sedf - link and activate it !!! *) +(* shouldn't work: label exists, but definition was finally rejected to to errors. *) section \Miscellaneous\ diff --git a/test/conceptual/Attributes.thy b/test/conceptual/Attributes.thy index 1d46c1de..3a9e917f 100644 --- a/test/conceptual/Attributes.thy +++ b/test/conceptual/Attributes.thy @@ -10,10 +10,11 @@ print_doc_items (* corresponds to low-level accesses : *) ML\ -val ({tab = x, ...},y,_)= DOF_core.get_data @{context}; -Symtab.dest x; +val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...} + = DOF_core.get_data @{context}; +Symtab.dest docitem_tab; "=============================================="; -Symtab.dest y; +Symtab.dest docclass_tab; \ text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\ sdfsdfs sdfsdf sdfsdf @{thm refl} \ @@ -63,34 +64,34 @@ text\A not too trivial test: default y -> []. The latter wins at access time. Then @{term "t"}: creation of a multi inheritance object omega, triple updates, the last one wins.\ -ML\val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg}); - val t = HOLogic.dest_string (@{docitem_attr x::omega}); \ +ML\val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::dfgdfg}); + val t = HOLogic.dest_string (@{docitem_attribute x::omega}); \ section\Mutation of Attibutes in DocItems\ -ML\ val Const ("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attr a2::omega} \ +ML\ val Const ("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attribute a2::omega} \ update_instance*[omega::E, a2+="1"] -ML\ val Const ("Groups.one_class.one", @{typ "int"})= @{docitem_attr a2::omega} \ +ML\ val Const ("Groups.one_class.one", @{typ "int"})= @{docitem_attribute a2::omega} \ update_instance*[omega::E, a2+="6"] -ML\ @{docitem_attr a2::omega} \ -ML\ HOLogic.dest_number @{docitem_attr a2::omega} \ +ML\ @{docitem_attribute a2::omega} \ +ML\ HOLogic.dest_number @{docitem_attribute a2::omega} \ update_instance*[omega::E, x+="''inition''"] -ML\ val s = HOLogic.dest_string ( @{docitem_attr x::omega}) \ +ML\ val s = HOLogic.dest_string ( @{docitem_attribute x::omega}) \ update_instance*[omega::E, y+="[''defini'',''tion'']"] update_instance*[omega::E, y+="[''en'']"] -ML\ val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::omega}); \ +ML\ val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::omega}); \ section\Simulation of a Monitor\ @@ -98,19 +99,18 @@ open_monitor*[figs1::figure_group, anchor="''fig-demo''", caption="''Sample ''"] -figure*[fig_A::figure, spawn_columns=False,relative_width="''90''", +figure*[fig_A::figure, spawn_columns=False,relative_width="90", src="''figures/A.png''"] \ The A train \ldots \ -update_instance*[figs1::figure_group, trace+="[figure]"](* simulation : will disappear *) -figure*[fig_B::figure, spawn_columns=False,relative_width="''90''", +figure*[fig_B::figure, spawn_columns=False,relative_width="90", src="''figures/B.png''"] \ The B train \ldots \ -update_instance*[figs1::figure_group, trace+="[figure]"](* simulation : will disappear *) -close_monitor*[fig1] +close_monitor*[figs1] -ML\ map (fn Const(s,_) => s) (HOLogic.dest_list @{docitem_attr trace::figs1}) \ +text\Resulting trace in figs1: \ +ML\@{trace_attribute figs1}\ print_doc_items diff --git a/test/conceptual/Concept_ExampleInvariant.thy b/test/conceptual/Concept_ExampleInvariant.thy new file mode 100644 index 00000000..1650d01a --- /dev/null +++ b/test/conceptual/Concept_ExampleInvariant.thy @@ -0,0 +1,109 @@ +chapter\Setting and modifying attributes of doc-items\ + +theory Concept_ExampleInvariant + imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *) +begin + +section\Example: Standard Class Invariant\ + +text\Status:\ +print_doc_classes +print_doc_items + + +text\Watch out: The current programming interface to document class invariants is pretty low-level: +\<^item> No inheritance principle +\<^item> No high-level notation in HOL +\<^item> Typing on ML level is assumed to be correct. +The implementor of an ontology must know what he does ... +\ + +text\Setting a sample invariant, which simply produces some side-effect:\ +setup\DOF_core.update_class_invariant "Conceptual.A" (fn oid => + fn {is_monitor = b} => + fn ctxt => + (writeln ("sample echo : "^oid); true))\ + +subsection*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ + + +text\Setting a sample invariant, referring to attribute value "x":\ +ML\fun check_A_invariant oid {is_monitor:bool} ctxt = + let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here} + val (@{typ "int"},x_value) = HOLogic.dest_number term + in if x_value > 5 then error("class A invariant violation") else true end +\ + +setup\DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\ + +(* test : should fail : *) +subsection*[c::A, x = "6"] \ Lorem ipsum dolor sit amet, ... \ + + +subsection*[d::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ + +(* test : update should fail : *) +update_instance*[d::A, x += "1"] + + +section\Example: Monitor Class Invariant\ + +text\Of particular interest are class invariants attached to monitor classes: since the +latter manage a trace-attribute, a class invariant on them can assure a global form of consistency. +It is possible to express: +\<^item> that attributes of a document element must satisfy particular conditions depending on the + prior document elements --- as long they have been observed in a monitor. +\<^item> non-regular properties on a trace not expressible in a regular expression + (like balanced ness of opening and closing text elements) +\<^item> etc. +\ + +text\A simple global trace-invariant is expressed in the following: it requires +that instances of class C occur more often as those of class D; note that this is meant +to take sub-classing into account: +\ + +ML\fun check_M_invariant oid {is_monitor} ctxt = + let val term = AttributeAccess.calc_attr_access ctxt "trace" oid @{here} + fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) + val string_pair_list = map conv (HOLogic.dest_list term) + val cid_list = map fst string_pair_list + val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) + fun is_C x = DOF_core.is_subclass ctxt' x "Conceptual.C" + fun is_D x = DOF_core.is_subclass ctxt' x "Conceptual.D" + val n = length (filter is_C cid_list) + val m = length (filter is_D cid_list) + in if m > n then error("class M invariant violation") else true end +\ + +setup\DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\ + +open_monitor*[struct::M] + + +section*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ + +text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ + +text*[d1::E, a1 = "X3"] \ ... phasellus amet id massa nunc, pede suscipit repellendus, ... \ + +text*[c2::C, x = "''delta''"] \ ... in ut tortor eleifend augue pretium consectetuer... \ + +section*[f::E] \ Lectus accumsan velit ultrices, ... }\ + +(* test : close_monitor should fail : *) +section*[f2::E] \ Lectus accumsan velit ultrices, ... }\ + +ML\val term = AttributeAccess.calc_attr_access (Context.Proof @{context}) "trace" "struct" @{here}; + fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) + val string_pair_list = map conv (HOLogic.dest_list term) + \ +(* trace example *) +text\Setting a sample invariant, referring to attribute value "x":\ + + +close_monitor*[struct] + + +end + \ No newline at end of file diff --git a/test/simple/Example.thy b/test/simple/Example.thy index 963d5e25..583bb5eb 100644 --- a/test/simple/Example.thy +++ b/test/simple/Example.thy @@ -95,8 +95,7 @@ section*[sedf::requirement, long_name = "None::string option"] jump to its definition. *} text\\label{sedf}\ (* Hack to make the LaTeX-ing running. Should disappear. *) -section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting, -but wrong doc_class constraint. *} +section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with undefined attributes. *} section{* Text Antiquotation Infrastructure ... *}