Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline failed
Details
ci/woodpecker/push/build Pipeline failed
Details
This commit is contained in:
commit
e1f143d151
|
@ -74,7 +74,7 @@ abstract*[abs::abstract, keywordlist="[''Ontology'',''Ontological Modeling'',''I
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
section*[intro::introduction]\<open> Introduction \<close>
|
section*[intro::introduction]\<open> Introduction \<close>
|
||||||
text*[introtext::introduction]\<open>
|
text*[introtext::introduction, level = "Some 1"]\<open>
|
||||||
The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\<close> is perhaps the
|
The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\<close> is perhaps the
|
||||||
most pervasive challenge in the digitization of knowledge and its
|
most pervasive challenge in the digitization of knowledge and its
|
||||||
propagation. This challenge incites numerous research efforts
|
propagation. This challenge incites numerous research efforts
|
||||||
|
@ -123,7 +123,7 @@ declare_reference*[ontomod::text_section]
|
||||||
declare_reference*[ontopide::text_section]
|
declare_reference*[ontopide::text_section]
|
||||||
declare_reference*[conclusion::text_section]
|
declare_reference*[conclusion::text_section]
|
||||||
(*>*)
|
(*>*)
|
||||||
text*[plan::introduction]\<open> The plan of the paper is follows: we start by introducing the underlying
|
text*[plan::introduction, level="Some 1"]\<open> The plan of the paper is follows: we start by introducing the underlying
|
||||||
Isabelle system (@{text_section (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
Isabelle system (@{text_section (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
||||||
essentials of \<^isadof> and its ontology language (@{text_section (unchecked) \<open>isadof\<close>}).
|
essentials of \<^isadof> and its ontology language (@{text_section (unchecked) \<open>isadof\<close>}).
|
||||||
It follows @{text_section (unchecked) \<open>ontomod\<close>}, where we present three application
|
It follows @{text_section (unchecked) \<open>ontomod\<close>}, where we present three application
|
||||||
|
@ -133,7 +133,7 @@ conclusions and discuss related work in @{text_section (unchecked) \<open>conclu
|
||||||
|
|
||||||
section*[bgrnd::text_section,main_author="Some(@{docitem ''bu''}::author)"]
|
section*[bgrnd::text_section,main_author="Some(@{docitem ''bu''}::author)"]
|
||||||
\<open> Background: The Isabelle System \<close>
|
\<open> Background: The Isabelle System \<close>
|
||||||
text*[background::introduction]\<open>
|
text*[background::introduction, level="Some 1"]\<open>
|
||||||
While Isabelle is widely perceived as an interactive theorem prover
|
While Isabelle is widely perceived as an interactive theorem prover
|
||||||
for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we
|
for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we
|
||||||
would like to emphasize the view that Isabelle is far more than that:
|
would like to emphasize the view that Isabelle is far more than that:
|
||||||
|
@ -162,7 +162,7 @@ figure*[architecture::figure,relative_width="100",src="''figures/isabelle-archit
|
||||||
asynchronous communication between the Isabelle system and
|
asynchronous communication between the Isabelle system and
|
||||||
the IDE (right-hand side). \<close>
|
the IDE (right-hand side). \<close>
|
||||||
|
|
||||||
text*[blug::introduction]\<open> The Isabelle system architecture shown in @{figure \<open>architecture\<close>}
|
text*[blug::introduction, level="Some 1"]\<open> The Isabelle system architecture shown in @{figure \<open>architecture\<close>}
|
||||||
comes with many layers, with Standard ML (SML) at the bottom layer as implementation
|
comes with many layers, with Standard ML (SML) at the bottom layer as implementation
|
||||||
language. The architecture actually foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which
|
language. The architecture actually foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which
|
||||||
resides in the SML structure \<^ML_structure>\<open>Context\<close>. This structure provides a kind of container called
|
resides in the SML structure \<^ML_structure>\<open>Context\<close>. This structure provides a kind of container called
|
||||||
|
@ -194,7 +194,7 @@ For the antiquotation \inlineisar+\at{value "fac 5"}+ we assume the usual defin
|
||||||
\inlineisar+fac+ in HOL.
|
\inlineisar+fac+ in HOL.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text*[anti]\<open> Thus, antiquotations can refer to formal content, can be type-checked before being
|
text*[anti::introduction, level = "Some 1"]\<open> Thus, antiquotations can refer to formal content, can be type-checked before being
|
||||||
displayed and can be used for calculations before actually being typeset. When editing,
|
displayed and can be used for calculations before actually being typeset. When editing,
|
||||||
Isabelle's PIDE offers auto-completion and error-messages while typing the above
|
Isabelle's PIDE offers auto-completion and error-messages while typing the above
|
||||||
\<^emph>\<open>semi-formal\<close> content. \<close>
|
\<^emph>\<open>semi-formal\<close> content. \<close>
|
||||||
|
|
|
@ -52,7 +52,7 @@ abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Alg
|
||||||
\<close>
|
\<close>
|
||||||
text\<open>\<close>
|
text\<open>\<close>
|
||||||
section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\<open> Introduction \<close>
|
section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\<open> Introduction \<close>
|
||||||
text*[introtext::introduction]\<open>
|
text*[introtext::introduction, level="Some 1"]\<open>
|
||||||
Communicating Sequential Processes (\<^csp>) is a language
|
Communicating Sequential Processes (\<^csp>) is a language
|
||||||
to specify and verify patterns of interaction of concurrent systems.
|
to specify and verify patterns of interaction of concurrent systems.
|
||||||
Together with CCS and LOTOS, it belongs to the family of \<^emph>\<open>process algebras\<close>.
|
Together with CCS and LOTOS, it belongs to the family of \<^emph>\<open>process algebras\<close>.
|
||||||
|
@ -154,7 +154,7 @@ processes \<open>Skip\<close> (successful termination) and \<open>Stop\<close> (
|
||||||
\<open>\<T>(Skip) = \<T>(Stop) = {[]}\<close>.
|
\<open>\<T>(Skip) = \<T>(Stop) = {[]}\<close>.
|
||||||
Note that the trace sets, representing all \<^emph>\<open>partial\<close> history, is in general prefix closed.\<close>
|
Note that the trace sets, representing all \<^emph>\<open>partial\<close> history, is in general prefix closed.\<close>
|
||||||
|
|
||||||
text*[ex1::math_example, status=semiformal] \<open>
|
text*[ex1::math_example, status=semiformal, level="Some 1"] \<open>
|
||||||
Let two processes be defined as follows:
|
Let two processes be defined as follows:
|
||||||
|
|
||||||
\<^enum> \<open>P\<^sub>d\<^sub>e\<^sub>t = (a \<rightarrow> Stop) \<box> (b \<rightarrow> Stop)\<close>
|
\<^enum> \<open>P\<^sub>d\<^sub>e\<^sub>t = (a \<rightarrow> Stop) \<box> (b \<rightarrow> Stop)\<close>
|
||||||
|
@ -354,7 +354,7 @@ Roscoe and Brooks @{cite "Roscoe1992AnAO"} finally proposed another ordering, ca
|
||||||
that completeness could at least be assured for read-operations. This more complex ordering
|
that completeness could at least be assured for read-operations. This more complex ordering
|
||||||
is based on the concept \<^emph>\<open>refusals after\<close> a trace \<open>s\<close> and defined by \<open>\<R> P s \<equiv> {X | (s, X) \<in> \<F> P}\<close>.\<close>
|
is based on the concept \<^emph>\<open>refusals after\<close> a trace \<open>s\<close> and defined by \<open>\<R> P s \<equiv> {X | (s, X) \<in> \<F> P}\<close>.\<close>
|
||||||
|
|
||||||
Definition*[process_ordering, short_name="''process ordering''"]\<open>
|
Definition*[process_ordering, level= "Some 2", short_name="''process ordering''"]\<open>
|
||||||
We define \<open>P \<sqsubseteq> Q \<equiv> \<psi>\<^sub>\<D> \<and> \<psi>\<^sub>\<R> \<and> \<psi>\<^sub>\<M> \<close>, where
|
We define \<open>P \<sqsubseteq> Q \<equiv> \<psi>\<^sub>\<D> \<and> \<psi>\<^sub>\<R> \<and> \<psi>\<^sub>\<M> \<close>, where
|
||||||
\<^enum> \<open>\<psi>\<^sub>\<D> = \<D> P \<supseteq> \<D> Q \<close>
|
\<^enum> \<open>\<psi>\<^sub>\<D> = \<D> P \<supseteq> \<D> Q \<close>
|
||||||
\<^enum> \<open>\<psi>\<^sub>\<R> = s \<notin> \<D> P \<Rightarrow> \<R> P s = \<R> Q s\<close>
|
\<^enum> \<open>\<psi>\<^sub>\<R> = s \<notin> \<D> P \<Rightarrow> \<R> P s = \<R> Q s\<close>
|
||||||
|
@ -530,10 +530,10 @@ To handle termination better, we added two new processes \<open>CHAOS\<^sub>S\<^
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
(*<*) (* a test ...*)
|
(*<*) (* a test ...*)
|
||||||
text*[X22 ::math_content ]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<close>
|
text*[X22 ::math_content, level="Some 2" ]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<close>
|
||||||
text*[X32::"definition", mcc=defn]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
text*[X32::"definition", level="Some 2", mcc=defn]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||||
Definition*[X42]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
Definition*[X42, level="Some 2"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||||
Definition*[X52::"definition"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
Definition*[X52::"definition", level="Some 2"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||||
|
|
||||||
text\<open> The \<open>RUN\<close>-process defined @{math_content X22} represents the process that accepts all
|
text\<open> The \<open>RUN\<close>-process defined @{math_content X22} represents the process that accepts all
|
||||||
events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in two variants shown in
|
events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in two variants shown in
|
||||||
|
@ -541,11 +541,11 @@ events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in
|
||||||
stops or accepts any offered event, whereas \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> can additionally terminate.\<close>
|
stops or accepts any offered event, whereas \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> can additionally terminate.\<close>
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
||||||
Definition*[X2]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<close>
|
Definition*[X2, level="Some 2"]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<close>
|
||||||
Definition*[X3]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
Definition*[X3, level="Some 2"]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||||
Definition*[X4]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<close>
|
Definition*[X4, level="Some 2"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<close>
|
||||||
Definition*[X5]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> x \<in> A \<rightarrow> X)\<close> \<close>
|
Definition*[X5, level="Some 2"]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> x \<in> A \<rightarrow> X)\<close> \<close>
|
||||||
Definition*[X6]\<open>\<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. ((\<sqinter> x \<in> A \<rightarrow> X) \<sqinter> SKIP)\<close> \<close>
|
Definition*[X6, level="Some 2"]\<open>\<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. ((\<sqinter> x \<in> A \<rightarrow> X) \<sqinter> SKIP)\<close> \<close>
|
||||||
|
|
||||||
text\<open>In the following, we denote \<open> \<R>\<P> = {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>.
|
text\<open>In the following, we denote \<open> \<R>\<P> = {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>.
|
||||||
All five reference processes are divergence-free.
|
All five reference processes are divergence-free.
|
||||||
|
@ -607,16 +607,16 @@ handled separately. One contribution of our work is establish their precise rela
|
||||||
the Failure/Divergence Semantics of \<^csp>.\<close>
|
the Failure/Divergence Semantics of \<^csp>.\<close>
|
||||||
|
|
||||||
(* bizarre: Definition* does not work for this single case *)
|
(* bizarre: Definition* does not work for this single case *)
|
||||||
text*[X10::"definition"]\<open> \<open>deadlock\<^sub>-free P \<equiv> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close> \<close>
|
text*[X10::"definition", level="Some 2"]\<open> \<open>deadlock\<^sub>-free P \<equiv> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close> \<close>
|
||||||
|
|
||||||
text\<open>\<^noindent> A process \<open>P\<close> is deadlock-free if and only if after any trace \<open>s\<close> without \<open>\<surd>\<close>, the union of \<open>\<surd>\<close>
|
text\<open>\<^noindent> A process \<open>P\<close> is deadlock-free if and only if after any trace \<open>s\<close> without \<open>\<surd>\<close>, the union of \<open>\<surd>\<close>
|
||||||
and all events of \<open>P\<close> can never be a refusal set associated to \<open>s\<close>, which means that \<open>P\<close> cannot
|
and all events of \<open>P\<close> can never be a refusal set associated to \<open>s\<close>, which means that \<open>P\<close> cannot
|
||||||
be deadlocked after any non-terminating trace.
|
be deadlocked after any non-terminating trace.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"]
|
Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>", level="Some 2"]
|
||||||
\<open> \hfill \break \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<close>
|
\<open> \hfill \break \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<close>
|
||||||
Definition*[X11]\<open> \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close> \<close>
|
Definition*[X11, level="Some 2"]\<open> \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close> \<close>
|
||||||
|
|
||||||
text\<open> Recall that all five reference processes are livelock-free.
|
text\<open> Recall that all five reference processes are livelock-free.
|
||||||
We also have the following lemmas about the
|
We also have the following lemmas about the
|
||||||
|
@ -630,7 +630,7 @@ text\<open>
|
||||||
Finally, we proved the following theorem that confirms the relationship between the two vital
|
Finally, we proved the following theorem that confirms the relationship between the two vital
|
||||||
properties:
|
properties:
|
||||||
\<close>
|
\<close>
|
||||||
Theorem*[T2, short_name="''DF implies LF''"]
|
Theorem*[T2, short_name="''DF implies LF''", level="Some 2"]
|
||||||
\<open> \<open>deadlock_free P \<longrightarrow> livelock_free P\<close> \<close>
|
\<open> \<open>deadlock_free P \<longrightarrow> livelock_free P\<close> \<close>
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
|
@ -797,7 +797,7 @@ This normal form is closed under deterministic and communication operators.
|
||||||
The advantage of this format is that we can mimick the well-known product automata construction
|
The advantage of this format is that we can mimick the well-known product automata construction
|
||||||
for an arbitrary number of synchronized processes under normal form.
|
for an arbitrary number of synchronized processes under normal form.
|
||||||
We only show the case of the synchronous product of two processes: \<close>
|
We only show the case of the synchronous product of two processes: \<close>
|
||||||
text*[T3::"theorem", short_name="\<open>Product Construction\<close>"]\<open>
|
text*[T3::"theorem", short_name="\<open>Product Construction\<close>", level="Some 2"]\<open>
|
||||||
Parallel composition translates to normal form:
|
Parallel composition translates to normal form:
|
||||||
@{cartouche [display,indent=5]\<open>(P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>1,\<upsilon>\<^sub>1\<rbrakk> \<sigma>\<^sub>1) || (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>2,\<upsilon>\<^sub>2\<rbrakk> \<sigma>\<^sub>2) =
|
@{cartouche [display,indent=5]\<open>(P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>1,\<upsilon>\<^sub>1\<rbrakk> \<sigma>\<^sub>1) || (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>2,\<upsilon>\<^sub>2\<rbrakk> \<sigma>\<^sub>2) =
|
||||||
P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2). \<tau>\<^sub>1 \<sigma>\<^sub>1 \<inter> \<tau>\<^sub>2 \<sigma>\<^sub>2 , \<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2).\<lambda>e.(\<upsilon>\<^sub>1 \<sigma>\<^sub>1 e, \<upsilon>\<^sub>2 \<sigma>\<^sub>2 e)\<rbrakk> (\<sigma>\<^sub>1,\<sigma>\<^sub>2)\<close>}
|
P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2). \<tau>\<^sub>1 \<sigma>\<^sub>1 \<inter> \<tau>\<^sub>2 \<sigma>\<^sub>2 , \<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2).\<lambda>e.(\<upsilon>\<^sub>1 \<sigma>\<^sub>1 e, \<upsilon>\<^sub>2 \<sigma>\<^sub>2 e)\<rbrakk> (\<sigma>\<^sub>1,\<sigma>\<^sub>2)\<close>}
|
||||||
|
@ -817,7 +817,7 @@ states via the closure \<open>\<RR>\<close>, which is defined inductively over:
|
||||||
Thus, normalization leads to a new characterization of deadlock-freeness inspired
|
Thus, normalization leads to a new characterization of deadlock-freeness inspired
|
||||||
from automata theory. We formally proved the following theorem:\<close>
|
from automata theory. We formally proved the following theorem:\<close>
|
||||||
|
|
||||||
text*[T4::"theorem", short_name="\<open>DF vs. Reacheability\<close>"]
|
text*[T4::"theorem", short_name="\<open>DF vs. Reacheability\<close>", level="Some 2"]
|
||||||
\<open> If each reachable state \<open>s \<in> (\<RR> \<tau> \<upsilon>)\<close> has outgoing transitions,
|
\<open> If each reachable state \<open>s \<in> (\<RR> \<tau> \<upsilon>)\<close> has outgoing transitions,
|
||||||
the \<^csp> process is deadlock-free:
|
the \<^csp> process is deadlock-free:
|
||||||
@{cartouche [display,indent=10] \<open>\<forall>\<sigma> \<in> (\<RR> \<tau> \<upsilon> \<sigma>\<^sub>0). \<tau> \<sigma> \<noteq> {} \<Longrightarrow> deadlock_free (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>,\<upsilon>\<rbrakk> \<sigma>\<^sub>0)\<close>}
|
@{cartouche [display,indent=10] \<open>\<forall>\<sigma> \<in> (\<RR> \<tau> \<upsilon> \<sigma>\<^sub>0). \<tau> \<sigma> \<noteq> {} \<Longrightarrow> deadlock_free (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>,\<upsilon>\<rbrakk> \<sigma>\<^sub>0)\<close>}
|
||||||
|
|
|
@ -1041,10 +1041,11 @@ text\<open>
|
||||||
Ontological classes as described so far are too liberal in many situations.
|
Ontological classes as described so far are too liberal in many situations.
|
||||||
There is a first high-level syntax implementation for class invariants.
|
There is a first high-level syntax implementation for class invariants.
|
||||||
These invariants can be checked when an instance of the class is defined.
|
These invariants can be checked when an instance of the class is defined.
|
||||||
To enable the checking of the invariants, the \<^boxed_theory_text>\<open>invariants_checking\<close>
|
To enable the strict checking of the invariants,
|
||||||
|
the \<^boxed_theory_text>\<open>invariants_strict_checking\<close>
|
||||||
theory attribute must be set:
|
theory attribute must be set:
|
||||||
@{boxed_theory_text [display]\<open>
|
@{boxed_theory_text [display]\<open>
|
||||||
declare[[invariants_checking = true]]\<close>}
|
declare[[invariants_strict_checking = true]]\<close>}
|
||||||
|
|
||||||
For example, let's define the following two classes:
|
For example, let's define the following two classes:
|
||||||
@{boxed_theory_text [display]\<open>
|
@{boxed_theory_text [display]\<open>
|
||||||
|
@ -1104,8 +1105,15 @@ text\<open>
|
||||||
All specified constraints are already checked in the IDE of \<^dof> while editing.
|
All specified constraints are already checked in the IDE of \<^dof> while editing.
|
||||||
The invariant \<^boxed_theory_text>\<open>author_finite\<close> enforces that the user sets the
|
The invariant \<^boxed_theory_text>\<open>author_finite\<close> enforces that the user sets the
|
||||||
\<^boxed_theory_text>\<open>authored_by\<close> set.
|
\<^boxed_theory_text>\<open>authored_by\<close> set.
|
||||||
|
The invariants \<^theory_text>\<open>author_finite\<close> and \<^theory_text>\<open>establish_defined\<close> can not be checked directly
|
||||||
|
and need a little help.
|
||||||
|
We can set the \<open>invariants_checking_with_tactics\<close> theory attribute to help the checking.
|
||||||
|
It will enable a basic tactic, using unfold and auto:
|
||||||
|
@{boxed_theory_text [display]\<open>
|
||||||
|
declare[[invariants_checking_with_tactics = true]]\<close>}
|
||||||
There are still some limitations with this high-level syntax.
|
There are still some limitations with this high-level syntax.
|
||||||
For now, the high-level syntax does not support monitors (see \<^technical>\<open>sec:monitors\<close>).
|
For now, the high-level syntax does not support the checking of
|
||||||
|
specific monitor behaviors (see \<^technical>\<open>sec:monitors\<close>).
|
||||||
For example, one would like to delay a final error message till the
|
For example, one would like to delay a final error message till the
|
||||||
closing of a monitor.
|
closing of a monitor.
|
||||||
For this use-case you can use low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>).
|
For this use-case you can use low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>).
|
||||||
|
@ -1147,6 +1155,20 @@ text\<open>
|
||||||
instances of \<open>S\<close>.
|
instances of \<open>S\<close>.
|
||||||
\<close>
|
\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
|
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>\<open>strict_monitor_checking\<close> theory attribute:
|
||||||
|
@{boxed_theory_text [display]\<open>declare[[strict_monitor_checking = true]]\<close>}
|
||||||
|
It is possible to enable the tracing of free classes occurring inside the scope of a monitor by
|
||||||
|
enabling the \<^boxed_theory_text>\<open>free_class_in_monitor_checking\<close>
|
||||||
|
theory attribute:
|
||||||
|
@{boxed_theory_text [display]\<open>declare[[free_class_in_monitor_checking = true]]\<close>}
|
||||||
|
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>\<open>free_class_in_monitor_strict_checking\<close> theory attribute:
|
||||||
|
@{boxed_theory_text [display]\<open>declare[[free_class_in_monitor_strict_checking = true]]\<close>}
|
||||||
|
|
||||||
Monitored document sections can be nested and overlap; thus, it is
|
Monitored document sections can be nested and overlap; thus, it is
|
||||||
possible to combine the effect of different monitors. For example, it
|
possible to combine the effect of different monitors. For example, it
|
||||||
would be possible to refine the \<^boxed_theory_text>\<open>example\<close> section by its own
|
would be possible to refine the \<^boxed_theory_text>\<open>example\<close> section by its own
|
||||||
|
@ -1164,8 +1186,9 @@ text\<open>
|
||||||
header delimiting the borders of its representation. Class invariants
|
header delimiting the borders of its representation. Class invariants
|
||||||
on monitors allow for specifying structural properties on document
|
on monitors allow for specifying structural properties on document
|
||||||
sections.
|
sections.
|
||||||
For now, the high-level syntax of invariants is not supported for monitors and you must use
|
For now, the high-level syntax of invariants does not support the checking of
|
||||||
the low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>.\<close>
|
specific monitor behaviors like the one above and you must use
|
||||||
|
the low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>).\<close>
|
||||||
|
|
||||||
|
|
||||||
subsection*["sec:low_level_inv"::technical]\<open>ODL Low-level Class Invariants\<close>
|
subsection*["sec:low_level_inv"::technical]\<open>ODL Low-level Class Invariants\<close>
|
||||||
|
|
|
@ -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};
|
docclass_lazy_inv_tab=f docclass_lazy_inv_tab};
|
||||||
|
|
||||||
fun get_accepted_cids ({accepted_cids, ... } : open_monitor_info) = accepted_cids
|
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
|
fun get_automatas ({automatas, ... } : open_monitor_info) = automatas
|
||||||
|
|
||||||
|
|
||||||
|
@ -813,8 +815,14 @@ fun print_doc_class_tree ctxt P T =
|
||||||
val (strict_monitor_checking, strict_monitor_checking_setup)
|
val (strict_monitor_checking, strict_monitor_checking_setup)
|
||||||
= Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
|
= Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
|
||||||
|
|
||||||
val (invariants_checking, invariants_checking_setup)
|
val (free_class_in_monitor_checking, free_class_in_monitor_checking_setup)
|
||||||
= Attrib.config_bool \<^binding>\<open>invariants_checking\<close> (K false);
|
= Attrib.config_bool \<^binding>\<open>free_class_in_monitor_checking\<close> (K false);
|
||||||
|
|
||||||
|
val (free_class_in_monitor_strict_checking, free_class_in_monitor_strict_checking_setup)
|
||||||
|
= Attrib.config_bool \<^binding>\<open>free_class_in_monitor_strict_checking\<close> (K false);
|
||||||
|
|
||||||
|
val (invariants_strict_checking, invariants_strict_checking_setup)
|
||||||
|
= Attrib.config_bool \<^binding>\<open>invariants_strict_checking\<close> (K false);
|
||||||
|
|
||||||
val (invariants_checking_with_tactics, invariants_checking_with_tactics_setup)
|
val (invariants_checking_with_tactics, invariants_checking_with_tactics_setup)
|
||||||
= Attrib.config_bool \<^binding>\<open>invariants_checking_with_tactics\<close> (K false);
|
= Attrib.config_bool \<^binding>\<open>invariants_checking_with_tactics\<close> (K false);
|
||||||
|
@ -825,7 +833,9 @@ end (* struct *)
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
setup\<open>DOF_core.strict_monitor_checking_setup
|
setup\<open>DOF_core.strict_monitor_checking_setup
|
||||||
#> DOF_core.invariants_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\<close>
|
#> DOF_core.invariants_checking_with_tactics_setup\<close>
|
||||||
|
|
||||||
section\<open> Syntax for Term Annotation Antiquotations (TA)\<close>
|
section\<open> Syntax for Term Annotation Antiquotations (TA)\<close>
|
||||||
|
@ -948,6 +958,7 @@ structure ISA_core =
|
||||||
struct
|
struct
|
||||||
|
|
||||||
fun err msg pos = error (msg ^ Position.here pos);
|
fun err msg pos = error (msg ^ Position.here pos);
|
||||||
|
fun warn msg pos = warning (msg ^ Position.here pos);
|
||||||
|
|
||||||
fun check_path check_file ctxt dir (name, pos) =
|
fun check_path check_file ctxt dir (name, pos) =
|
||||||
let
|
let
|
||||||
|
@ -1433,7 +1444,7 @@ fun create_default_object thy class_name =
|
||||||
in list_comb (make_const, (tag_attr (serial()))::class_list'') end
|
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
|
let
|
||||||
val cid_long = DOF_core.read_cid_global thy cid
|
val cid_long = DOF_core.read_cid_global thy cid
|
||||||
|
|
||||||
|
@ -1443,10 +1454,10 @@ fun check_classref {is_monitor=is_monitor} (SOME(cid,pos')) thy =
|
||||||
else ()
|
else ()
|
||||||
val markup = docclass_markup false cid id (Binding.pos_of bind_target);
|
val markup = docclass_markup false cid id (Binding.pos_of bind_target);
|
||||||
val ctxt = Context.Theory thy
|
val ctxt = Context.Theory thy
|
||||||
val _ = Context_Position.report_generic ctxt pos' markup;
|
val _ = Context_Position.report_generic ctxt pos markup;
|
||||||
in cid_long
|
in (cid_long, pos)
|
||||||
end
|
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));
|
fun generalize_typ n = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,n),sort));
|
||||||
|
@ -1514,67 +1525,104 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long
|
||||||
end
|
end
|
||||||
in Sign.certify_term thy (fold read_assn S term) 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
|
fun msg thy txt pos = if Config.get_global thy DOF_core.strict_monitor_checking
|
||||||
then error txt
|
then ISA_core.err txt pos
|
||||||
else warning txt
|
else ISA_core.warn txt pos
|
||||||
|
|
||||||
fun register_oid_cid_in_open_monitors oid pos cid_long thy =
|
fun register_oid_cid_in_open_monitors oid pos cid_pos thy =
|
||||||
let val {monitor_tab,...} = DOF_core.get_data_global thy
|
let val {monitor_tab,...} = DOF_core.get_data_global thy
|
||||||
fun is_enabled (n, info) =
|
val cid_long= fst cid_pos
|
||||||
if exists (DOF_core.is_subclass_global thy cid_long)
|
val pos' = snd cid_pos
|
||||||
(DOF_core.get_accepted_cids info)
|
fun is_enabled (n, info) =
|
||||||
then SOME n
|
if exists (DOF_core.is_subclass_global thy cid_long)
|
||||||
else NONE
|
(DOF_core.get_alphabet info)
|
||||||
(* filtering those monitors with automata, whose alphabet contains the
|
then SOME n
|
||||||
cid of this oid. The enabled ones were selected and moved to their successor state
|
else if Config.get_global thy DOF_core.free_class_in_monitor_strict_checking
|
||||||
along the super-class id. The evaluation is in parallel, simulating a product
|
orelse Config.get_global thy DOF_core.free_class_in_monitor_checking
|
||||||
semantics without expanding the subclass relationship. *)
|
then SOME n
|
||||||
fun is_enabled_for_cid moid =
|
else NONE
|
||||||
let val {accepted_cids, automatas, ...} =
|
(* filtering those monitors with automata, whose alphabet contains the
|
||||||
the(Symtab.lookup monitor_tab moid)
|
cid of this oid. The enabled ones were selected and moved to their successor state
|
||||||
val indexS= 1 upto (length automatas)
|
along the super-class id. The evaluation is in parallel, simulating a product
|
||||||
val indexed_autoS = automatas ~~ indexS
|
semantics without expanding the subclass relationship. *)
|
||||||
fun check_for_cid (A,n) =
|
fun is_enabled_for_cid moid =
|
||||||
let val accS = (RegExpInterface.enabled A accepted_cids)
|
let val {accepted_cids, automatas, rejected_cids, ...} =
|
||||||
val is_subclass = DOF_core.is_subclass_global thy
|
the(Symtab.lookup monitor_tab moid)
|
||||||
val idx = find_index (is_subclass cid_long) accS
|
val indexS= 1 upto (length automatas)
|
||||||
in if idx < 0
|
val indexed_autoS = automatas ~~ indexS
|
||||||
then (msg thy ("monitor "^moid^"(" ^ Int.toString n
|
fun check_for_cid (A,n) =
|
||||||
^") not enabled for doc_class: "^cid_long);A)
|
let fun direct_super_class _ cid [] = cid
|
||||||
else RegExpInterface.next A accepted_cids (nth accS idx)
|
| 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
|
end
|
||||||
in (moid,map check_for_cid indexed_autoS) end
|
| SOME _ => (msg thy ("accepts clause " ^ Int.toString n
|
||||||
val enabled_monitors = List.mapPartial is_enabled (Symtab.dest monitor_tab)
|
^ " of monitor " ^ moid
|
||||||
fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn,
|
^ " rejected doc_class: " ^ cid_long) pos';A))
|
||||||
Syntax.read_term_global thy rhs)
|
| SOME accepted => (case first_rejected of
|
||||||
val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")]
|
NONE => RegExpInterface.next A accepted_cids (accepted)
|
||||||
val assns' = map conv_attrs trace_attr
|
| SOME rejected =>
|
||||||
fun cid_of oid = #cid(the(DOF_core.get_object_global oid thy))
|
if DOF_core.is_subclass_global thy accepted rejected
|
||||||
fun def_trans_input_term oid =
|
then RegExpInterface.next A accepted_cids (accepted)
|
||||||
#1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns')
|
else (msg thy ("accepts clause " ^ Int.toString n
|
||||||
fun def_trans_value oid =
|
^ " of monitor " ^ moid
|
||||||
(#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns'))
|
^ " rejected doc_class: " ^ cid_long) pos';A))
|
||||||
#> value (Proof_Context.init_global thy)
|
end
|
||||||
val _ = if null enabled_monitors then () else writeln "registrating in monitors ..."
|
in (moid,map check_for_cid indexed_autoS) end
|
||||||
val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors;
|
val enabled_monitors = List.mapPartial is_enabled (Symtab.dest monitor_tab)
|
||||||
(* check that any transition is possible : *)
|
fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn,
|
||||||
fun inst_class_inv x = DOF_core.get_class_invariant(cid_of x) thy x {is_monitor=false}
|
Syntax.read_term_global thy rhs)
|
||||||
fun class_inv_checks ctxt = map (fn x => inst_class_inv x ctxt) enabled_monitors
|
val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")]
|
||||||
val delta_autoS = map is_enabled_for_cid enabled_monitors;
|
val assns' = map conv_attrs trace_attr
|
||||||
fun update_info (n, aS) (tab: DOF_core.monitor_tab) =
|
fun cid_of oid = #cid(the(DOF_core.get_object_global oid thy))
|
||||||
let val {accepted_cids,rejected_cids,...} = the(Symtab.lookup tab n)
|
fun def_trans_input_term oid =
|
||||||
in Symtab.update(n, {accepted_cids=accepted_cids,
|
#1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns')
|
||||||
rejected_cids=rejected_cids,
|
fun def_trans_value oid =
|
||||||
automatas=aS}) tab end
|
(#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns'))
|
||||||
fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans_input_term mon_oid) (def_trans_value mon_oid)
|
#> value (Proof_Context.init_global thy)
|
||||||
val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS)
|
val _ = if null enabled_monitors then () else writeln "registrating in monitors ..."
|
||||||
in thy |> (* update traces of all enabled monitors *)
|
val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors;
|
||||||
fold (update_trace) (enabled_monitors)
|
(* check that any transition is possible : *)
|
||||||
|> (* check class invariants of enabled monitors *)
|
fun inst_class_inv x = DOF_core.get_class_invariant(cid_of x) thy x {is_monitor=false}
|
||||||
(fn thy => (class_inv_checks (Context.Theory thy); thy))
|
fun class_inv_checks ctxt = map (fn x => inst_class_inv x ctxt) enabled_monitors
|
||||||
|> (* update the automata of enabled monitors *)
|
val delta_autoS = map is_enabled_for_cid enabled_monitors;
|
||||||
DOF_core.map_data_global(update_automatons)
|
fun update_info (n, aS) (tab: DOF_core.monitor_tab) =
|
||||||
end
|
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 =
|
fun check_invariants thy oid =
|
||||||
let
|
let
|
||||||
|
@ -1600,11 +1648,12 @@ fun check_invariants thy oid =
|
||||||
end
|
end
|
||||||
fun check_invariants' ((inv_name, pos), term) =
|
fun check_invariants' ((inv_name, pos), term) =
|
||||||
let val ctxt = Proof_Context.init_global thy
|
let val ctxt = Proof_Context.init_global thy
|
||||||
|
val trivial_true = \<^term>\<open>True\<close> |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
|
||||||
val evaluated_term = value ctxt term
|
val evaluated_term = value ctxt term
|
||||||
handle ERROR e =>
|
handle ERROR e =>
|
||||||
if (String.isSubstring "Wellsortedness error" e)
|
if (String.isSubstring "Wellsortedness error" e)
|
||||||
andalso (Config.get_global thy DOF_core.invariants_checking_with_tactics)
|
andalso (Config.get_global thy DOF_core.invariants_checking_with_tactics)
|
||||||
then (warning("Invariants checking uses proof tactics");
|
then (warning("Invariants checking uses proof tactics");
|
||||||
let val prop_term = HOLogic.mk_Trueprop term
|
let val prop_term = HOLogic.mk_Trueprop term
|
||||||
val thms = Proof_Context.get_thms ctxt (inv_name ^ def_suffixN)
|
val thms = Proof_Context.get_thms ctxt (inv_name ^ def_suffixN)
|
||||||
(* Get the make definition (def(1) of the record) *)
|
(* Get the make definition (def(1) of the record) *)
|
||||||
|
@ -1614,22 +1663,37 @@ fun check_invariants thy oid =
|
||||||
(K ((unfold_tac ctxt thms') THEN (auto_tac ctxt)))
|
(K ((unfold_tac ctxt thms') THEN (auto_tac ctxt)))
|
||||||
|> Thm.close_derivation \<^here>
|
|> Thm.close_derivation \<^here>
|
||||||
handle ERROR e =>
|
handle ERROR e =>
|
||||||
ISA_core.err ("Invariant "
|
let
|
||||||
|
val msg_intro = "Invariant "
|
||||||
^ inv_name
|
^ inv_name
|
||||||
^ " failed to be checked using proof tactics"
|
^ " failed to be checked using proof tactics"
|
||||||
^ " with error: "
|
^ " with error:\n"
|
||||||
^ e) pos
|
in
|
||||||
|
if Config.get_global thy DOF_core.invariants_strict_checking
|
||||||
|
then ISA_core.err (msg_intro ^ e) pos
|
||||||
|
else (ISA_core.warn (msg_intro ^ e) pos; trivial_true) end
|
||||||
(* If Goal.prove does not fail, then the evaluation is considered True,
|
(* If Goal.prove does not fail, then the evaluation is considered True,
|
||||||
else an error is triggered by Goal.prove *)
|
else an error is triggered by Goal.prove *)
|
||||||
in @{term True} end)
|
in @{term True} end)
|
||||||
else ISA_core.err ("Fail to check invariant "
|
else \<^term>\<open>True \<Longrightarrow> True\<close>
|
||||||
^ inv_name
|
in case evaluated_term of
|
||||||
^ ". Try to activate invariants_checking_with_tactics.") pos
|
\<^term>\<open>True\<close> => ((inv_name, pos), term)
|
||||||
in (if evaluated_term = \<^term>\<open>True\<close>
|
| \<^term>\<open>True \<Longrightarrow> True\<close> =>
|
||||||
then ((inv_name, pos), term)
|
let val msg_intro = "Fail to check invariant "
|
||||||
else ISA_core.err ("Invariant " ^ inv_name ^ " violated") pos)
|
^ inv_name
|
||||||
|
^ ".\nMaybe you can try "
|
||||||
|
^ "to activate invariants_checking_with_tactics\n"
|
||||||
|
^ "if your invariant is checked against doc_class algebraic "
|
||||||
|
^ "types like 'doc_class list' or 'doc_class set'"
|
||||||
|
in if Config.get_global thy DOF_core.invariants_strict_checking
|
||||||
|
then ISA_core.err (msg_intro) pos
|
||||||
|
else (ISA_core.warn (msg_intro) pos; ((inv_name, pos), term)) end
|
||||||
|
| _ => let val msg_intro = "Invariant " ^ inv_name ^ " violated"
|
||||||
|
in if Config.get_global thy DOF_core.invariants_strict_checking
|
||||||
|
then ISA_core.err msg_intro pos
|
||||||
|
else (ISA_core.warn msg_intro pos; ((inv_name, pos), term)) end
|
||||||
end
|
end
|
||||||
val _ = map check_invariants' inv_and_apply_list
|
val _ = map check_invariants' inv_and_apply_list
|
||||||
in thy end
|
in thy end
|
||||||
|
|
||||||
fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos doc_attrs thy =
|
fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos doc_attrs thy =
|
||||||
|
@ -1638,21 +1702,21 @@ 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);
|
val _ = Position.report pos (docref_markup true oid id pos);
|
||||||
(* creates a markup label for this position and reports it to the PIDE framework;
|
(* 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. *)
|
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
|
val vcid = case cid_pos of NONE => NONE
|
||||||
| SOME (cid,_) => if (DOF_core.is_virtual cid thy)
|
| SOME (cid,_) => if (DOF_core.is_virtual cid thy)
|
||||||
then SOME (DOF_core.parse_cid_global thy cid)
|
then SOME (DOF_core.parse_cid_global thy cid)
|
||||||
else NONE
|
else NONE
|
||||||
val value_terms = if (cid_long = DOF_core.default_cid)
|
val value_terms = if default_cid
|
||||||
then let
|
then let
|
||||||
val undefined_value = Free ("Undefined_Value", \<^Type>\<open>unit\<close>)
|
val undefined_value = Free ("Undefined_Value", \<^Type>\<open>unit\<close>)
|
||||||
in (undefined_value, undefined_value) end
|
in (undefined_value, undefined_value) end
|
||||||
(*
|
(* Handle initialization of docitem without a class associated,
|
||||||
Handle initialization of docitem without a class associated,
|
for example when you just want a document element to be referenceable
|
||||||
for example when you just want a document element to be referenceable
|
without using the burden of ontology classes.
|
||||||
without using the burden of ontology classes.
|
ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> *)
|
||||||
ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close>
|
|
||||||
*)
|
|
||||||
else let
|
else let
|
||||||
val defaults_init = create_default_object thy cid_long
|
val defaults_init = create_default_object thy cid_long
|
||||||
fun conv (na, _(*ty*), term) =(Binding.name_of na, Binding.pos_of na, "=", term);
|
fun conv (na, _(*ty*), term) =(Binding.name_of na, Binding.pos_of na, "=", term);
|
||||||
|
@ -1678,15 +1742,21 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
|
||||||
id = id,
|
id = id,
|
||||||
cid = cid_long,
|
cid = cid_long,
|
||||||
vcid = vcid})
|
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)
|
|> (fn thy => if #is_monitor(is_monitor)
|
||||||
then (((DOF_core.get_class_eager_invariant cid_long thy oid) is_monitor
|
then (((DOF_core.get_class_eager_invariant cid_long thy oid) is_monitor
|
||||||
o Context.Theory) thy; thy)
|
o Context.Theory) thy; thy)
|
||||||
else thy)
|
else thy)
|
||||||
|> (fn thy => (check_inv thy; thy))
|
|> (fn thy => (check_inv thy; thy))
|
||||||
|> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
|
(* Bypass checking of high-level invariants when the class default_cid = "text",
|
||||||
then check_invariants thy oid
|
the top (default) document class.
|
||||||
else thy)
|
We want the class default_cid to stay abstract
|
||||||
|
and not have the capability to be defined with attribute, invariants, etc.
|
||||||
|
Hence this bypass handles docitem without a class associated,
|
||||||
|
for example when you just want a document element to be referenceable
|
||||||
|
without using the burden of ontology classes.
|
||||||
|
ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> *)
|
||||||
|
|> (fn thy => if default_cid then thy else check_invariants thy oid)
|
||||||
end
|
end
|
||||||
|
|
||||||
end (* structure Docitem_Parser *)
|
end (* structure Docitem_Parser *)
|
||||||
|
@ -1848,8 +1918,9 @@ fun update_instance_command (((oid:string,pos),cid_pos),
|
||||||
val _ = Context_Position.report ctxt pos markup;
|
val _ = Context_Position.report ctxt pos markup;
|
||||||
in cid end
|
in cid end
|
||||||
| NONE => error("undefined doc_class.")
|
| 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
|
cid_pos thy
|
||||||
|
val cid_long = fst cid_pos'
|
||||||
val _ = if cid_long = DOF_core.default_cid orelse cid = cid_long
|
val _ = if cid_long = DOF_core.default_cid orelse cid = cid_long
|
||||||
then ()
|
then ()
|
||||||
else error("incompatible classes:"^cid^":"^cid_long)
|
else error("incompatible classes:"^cid^":"^cid_long)
|
||||||
|
@ -1870,9 +1941,7 @@ fun update_instance_command (((oid:string,pos),cid_pos),
|
||||||
in
|
in
|
||||||
thy |> DOF_core.update_value_global oid def_trans_input_term def_trans_value
|
thy |> DOF_core.update_value_global oid def_trans_input_term def_trans_value
|
||||||
|> check_inv
|
|> check_inv
|
||||||
|> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
|
|> (fn thy => Value_Command.Docitem_Parser.check_invariants thy oid)
|
||||||
then Value_Command.Docitem_Parser.check_invariants thy oid
|
|
||||||
else thy)
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
||||||
|
@ -1891,31 +1960,33 @@ fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Pars
|
||||||
in
|
in
|
||||||
case DOF_core.get_doc_class_global long_cid thy of
|
case DOF_core.get_doc_class_global long_cid thy of
|
||||||
SOME X => let val ralph = RegExpInterface.alphabet (#rejectS X)
|
SOME X => let val ralph = RegExpInterface.alphabet (#rejectS X)
|
||||||
val alph = RegExpInterface.ext_alphabet ralph (#rex X)
|
val aalph = RegExpInterface.alphabet (#rex X)
|
||||||
in (alph, map (RegExpInterface.rexp_term2da alph)(#rex X)) end
|
in (aalph, ralph, map (RegExpInterface.rexp_term2da aalph)(#rex X)) end
|
||||||
| NONE => error("Internal error: class id undefined. ")
|
| NONE => error("Internal error: class id undefined. ")
|
||||||
end
|
end
|
||||||
fun create_monitor_entry thy =
|
fun create_monitor_entry thy =
|
||||||
let val cid = case cid_pos of
|
let val cid = case cid_pos of
|
||||||
NONE => ISA_core.err ("You must specified a monitor class.") pos
|
NONE => ISA_core.err ("You must specified a monitor class.") pos
|
||||||
| SOME (cid, _) => cid
|
| SOME (cid, _) => cid
|
||||||
val (S, aS) = compute_enabled_set cid thy
|
val (accS, rejectS, aS) = compute_enabled_set cid thy
|
||||||
val info = {accepted_cids = S, rejected_cids = [], automatas = aS }
|
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)
|
in DOF_core.map_data_global(DOF_core.upd_monitor_tabs(Symtab.update(oid, info )))(thy)
|
||||||
end
|
end
|
||||||
in
|
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;
|
end;
|
||||||
|
|
||||||
|
|
||||||
fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|
fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|
||||||
doc_attrs: (((string*Position.T)*string)*string)list)) thy =
|
doc_attrs: (((string*Position.T)*string)*string)list)) thy =
|
||||||
let val {monitor_tab,...} = DOF_core.get_data_global 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
|
fun check_if_final aS = let val i = (find_index (not o RegExpInterface.final) aS) + 1
|
||||||
in if i >= 0
|
in if i >= 1
|
||||||
then
|
then
|
||||||
Value_Command.Docitem_Parser.msg thy
|
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 ()
|
else ()
|
||||||
end
|
end
|
||||||
val _ = case Symtab.lookup monitor_tab oid of
|
val _ = case Symtab.lookup monitor_tab oid of
|
||||||
|
@ -1932,9 +2003,7 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|
||||||
in thy |> (fn thy => (check_lazy_inv thy; thy))
|
in thy |> (fn thy => (check_lazy_inv thy; thy))
|
||||||
|> update_instance_command args
|
|> update_instance_command args
|
||||||
|> (fn thy => (check_inv thy; thy))
|
|> (fn thy => (check_inv thy; thy))
|
||||||
|> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
|
|> (fn thy => Value_Command.Docitem_Parser.check_invariants thy oid)
|
||||||
then Value_Command.Docitem_Parser.check_invariants thy oid
|
|
||||||
else thy)
|
|
||||||
|> delete_monitor_entry
|
|> delete_monitor_entry
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
|
@ -177,4 +177,47 @@ text*[ sdfg :: F] \<open> Lorem ipsum @{thm refl}\<close>
|
||||||
text*[ xxxy ] \<open> Lorem ipsum @{F \<open>sdfg\<close>} rate @{thm refl}\<close>
|
text*[ xxxy ] \<open> Lorem ipsum @{F \<open>sdfg\<close>} rate @{thm refl}\<close>
|
||||||
close_monitor*[aaa]
|
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>\<close>
|
||||||
|
|
||||||
|
open_monitor*[test_monitor_M2::monitor_M]
|
||||||
|
|
||||||
|
text*[test_monitor_A1::test_monitor_A]\<open>\<close>
|
||||||
|
text*[testFree2::test_monitor_free]\<open>\<close>
|
||||||
|
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>
|
||||||
|
text*[testFree4::test_monitor_free]\<open>\<close>
|
||||||
|
text*[test_monitor_D1::test_monitor_D]\<open>\<close>
|
||||||
|
text*[testFree5::test_monitor_free]\<open>\<close>
|
||||||
|
text*[test_monitor_C1::test_monitor_C]\<open>\<close>
|
||||||
|
text*[testFree6::test_monitor_free]\<open>\<close>
|
||||||
|
|
||||||
|
close_monitor*[test_monitor_M2]
|
||||||
|
|
||||||
|
close_monitor*[test_monitor_M]
|
||||||
|
|
||||||
|
end
|
||||||
|
|
|
@ -69,7 +69,7 @@ which we formalize into:\<close>
|
||||||
doc_class text_section = text_element +
|
doc_class text_section = text_element +
|
||||||
main_author :: "author option" <= None
|
main_author :: "author option" <= None
|
||||||
fixme_list :: "string list" <= "[]"
|
fixme_list :: "string list" <= "[]"
|
||||||
level :: "int option" <= "None"
|
level :: "int option" <= "None"
|
||||||
(* this attribute enables doc-notation support section* etc.
|
(* this attribute enables doc-notation support section* etc.
|
||||||
we follow LaTeX terminology on levels
|
we follow LaTeX terminology on levels
|
||||||
part = Some -1
|
part = Some -1
|
||||||
|
|
|
@ -173,9 +173,20 @@ text\<open> @{docitem_attribute y::omega} \<close>
|
||||||
|
|
||||||
section\<open>Simulation of a Monitor\<close>
|
section\<open>Simulation of a Monitor\<close>
|
||||||
|
|
||||||
|
declare[[free_class_in_monitor_checking]]
|
||||||
|
|
||||||
|
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,
|
open_monitor*[figs1::figure_group,
|
||||||
caption="''Sample ''"]
|
caption="''Sample ''"]
|
||||||
|
ML\<open>
|
||||||
|
val thy = \<^theory>
|
||||||
|
val {monitor_tab,...} = DOF_core.get_data_global thy
|
||||||
|
\<close>
|
||||||
|
text*[testFreeA::A]\<open>\<close>
|
||||||
figure*[fig_A::figure, spawn_columns=False,
|
figure*[fig_A::figure, spawn_columns=False,
|
||||||
relative_width="90",
|
relative_width="90",
|
||||||
src="''figures/A.png''"]
|
src="''figures/A.png''"]
|
||||||
|
@ -185,6 +196,47 @@ figure*[fig_B::figure,
|
||||||
spawn_columns=False,relative_width="90",
|
spawn_columns=False,relative_width="90",
|
||||||
src="''figures/B.png''"]
|
src="''figures/B.png''"]
|
||||||
\<open> The B train \ldots \<close>
|
\<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 C 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 D 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*[testRejected1::figure_group, caption="''figures/A.png''"]
|
||||||
|
\<open> The A train \ldots \<close>
|
||||||
|
|
||||||
|
figure*[fig_E::figure,
|
||||||
|
spawn_columns=False,relative_width="90",
|
||||||
|
src="''figures/B.png''"]
|
||||||
|
\<open> The E train \ldots \<close>
|
||||||
|
close_monitor*[figs4]
|
||||||
|
close_monitor*[figs2]
|
||||||
|
text*[testRejected2::figure_group, caption="''figures/A.png''"]
|
||||||
|
\<open> The A train \ldots \<close>
|
||||||
|
|
||||||
close_monitor*[figs1]
|
close_monitor*[figs1]
|
||||||
|
|
||||||
|
@ -199,7 +251,8 @@ term*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
|
||||||
value*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
|
value*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
|
||||||
term*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
|
term*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
|
||||||
value*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
|
value*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
|
||||||
value*\<open>(map fst @{trace-attribute \<open>aaa\<close>}) \<close>
|
term*\<open>map fst @{trace-attribute \<open>test_monitor_M\<close>}\<close>
|
||||||
|
value*\<open>map fst @{trace-attribute \<open>test_monitor_M\<close>}\<close>
|
||||||
|
|
||||||
definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*"
|
definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*"
|
||||||
value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>
|
value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>
|
||||||
|
|
|
@ -12,7 +12,7 @@ text\<open>
|
||||||
theory attribute must be set:\<close>
|
theory attribute must be set:\<close>
|
||||||
|
|
||||||
|
|
||||||
declare[[invariants_checking = true]]
|
declare[[invariants_strict_checking = true]]
|
||||||
|
|
||||||
text\<open>For example, let's define the following two classes:\<close>
|
text\<open>For example, let's define the following two classes:\<close>
|
||||||
|
|
||||||
|
@ -144,6 +144,6 @@ value*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \
|
||||||
|
|
||||||
declare[[invariants_checking_with_tactics = false]]
|
declare[[invariants_checking_with_tactics = false]]
|
||||||
|
|
||||||
declare[[invariants_checking = false]]
|
declare[[invariants_strict_checking = false]]
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
Loading…
Reference in New Issue