Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Continuous checking of class invariants of enabled monitors. 

Regression test suite revised.
This commit is contained in:
Burkhart Wolff 2018-12-04 14:28:59 +01:00
parent 5e7ac1c02e
commit 9c8d57e573
6 changed files with 142 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
Isa_DOF.thy
View File

@ -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

9
examples/conceptual/Concept_ExampleInvariant.thy
View File

@ -36,13 +36,11 @@ ML\<open>fun check_A_invariant oid {is_monitor:bool} ctxt =
setup\<open>DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\<close>
(* test : should fail : *)
subsection*[c::A, x = "6"] \<open> Lorem ipsum dolor sit amet, ... \<close>
subsection*[d::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
subsection*[d::A, x = "4"] \<open> Lorem ipsum dolor sit amet, ... \<close>
(* 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:
\<close>
ML\<open>fun check_M_invariant oid {is_monitor} ctxt =
ML\<open>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] \<open> Lectus accumsan velit ultrices, ... }\<clo
(* test : close_monitor should fail :
section*[f2::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
*)
ML\<open>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)

3
test/cenelec/Example.thy
View File

@ -97,8 +97,7 @@ text{* @{test_specification \<open>ass122\<close>} -- wrong: "reference ontologi
text{* Here is a reference to @{docref \<open>sedf\<close>} *}
(* 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 \<open>Miscellaneous\<close>

34
test/conceptual/Attributes.thy
View File

@ -10,10 +10,11 @@ print_doc_items
(* corresponds to low-level accesses : *)
ML\<open>
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;
\<close>
text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
@ -63,34 +64,34 @@ text\<open>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.\<close>
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg});
val t = HOLogic.dest_string (@{docitem_attr x::omega}); \<close>
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::dfgdfg});
val t = HOLogic.dest_string (@{docitem_attribute x::omega}); \<close>
section\<open>Mutation of Attibutes in DocItems\<close>
ML\<open> val Const ("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attr a2::omega} \<close>
ML\<open> val Const ("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attribute a2::omega} \<close>
update_instance*[omega::E, a2+="1"]
ML\<open> val Const ("Groups.one_class.one", @{typ "int"})= @{docitem_attr a2::omega} \<close>
ML\<open> val Const ("Groups.one_class.one", @{typ "int"})= @{docitem_attribute a2::omega} \<close>
update_instance*[omega::E, a2+="6"]
ML\<open> @{docitem_attr a2::omega} \<close>
ML\<open> HOLogic.dest_number @{docitem_attr a2::omega} \<close>
ML\<open> @{docitem_attribute a2::omega} \<close>
ML\<open> HOLogic.dest_number @{docitem_attribute a2::omega} \<close>
update_instance*[omega::E, x+="''inition''"]
ML\<open> val s = HOLogic.dest_string ( @{docitem_attr x::omega}) \<close>
ML\<open> val s = HOLogic.dest_string ( @{docitem_attribute x::omega}) \<close>
update_instance*[omega::E, y+="[''defini'',''tion'']"]
update_instance*[omega::E, y+="[''en'']"]
ML\<open> val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::omega}); \<close>
ML\<open> val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::omega}); \<close>
section\<open>Simulation of a Monitor\<close>
@ -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''"]
\<open> The A train \ldots \<close>
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''"]
\<open> The B train \ldots \<close>
update_instance*[figs1::figure_group, trace+="[figure]"](* simulation : will disappear *)
close_monitor*[fig1]
close_monitor*[figs1]
ML\<open> map (fn Const(s,_) => s) (HOLogic.dest_list @{docitem_attr trace::figs1}) \<close>
text\<open>Resulting trace in figs1: \<close>
ML\<open>@{trace_attribute figs1}\<close>
print_doc_items

109
test/conceptual/Concept_ExampleInvariant.thy Normal file
View File

@ -0,0 +1,109 @@
chapter\<open>Setting and modifying attributes of doc-items\<close>
theory Concept_ExampleInvariant
imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *)
begin
section\<open>Example: Standard Class Invariant\<close>
text\<open>Status:\<close>
print_doc_classes
print_doc_items
text\<open>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 ...
\<close>
text\<open>Setting a sample invariant, which simply produces some side-effect:\<close>
setup\<open>DOF_core.update_class_invariant "Conceptual.A" (fn oid =>
fn {is_monitor = b} =>
fn ctxt =>
(writeln ("sample echo : "^oid); true))\<close>
subsection*[b::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
ML\<open>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
\<close>
setup\<open>DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\<close>
(* test : should fail : *)
subsection*[c::A, x = "6"] \<open> Lorem ipsum dolor sit amet, ... \<close>
subsection*[d::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
(* test : update should fail : *)
update_instance*[d::A, x += "1"]
section\<open>Example: Monitor Class Invariant\<close>
text\<open>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.
\<close>
text\<open>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:
\<close>
ML\<open>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
\<close>
setup\<open>DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\<close>
open_monitor*[struct::M]
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
text*[d1::E, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
text*[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer... \<close>
section*[f::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
(* test : close_monitor should fail : *)
section*[f2::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
ML\<open>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)
\<close>
(* trace example *)
text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
close_monitor*[struct]
end

3
test/simple/Example.thy
View File

@ -95,8 +95,7 @@ section*[sedf::requirement, long_name = "None::string option"]
jump to its definition. *}
text\<open>\label{sedf}\<close> (* 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 ... *}