nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Section 5.5.

This commit is contained in:
Achim D. Brucker 2019-08-11 17:22:22 +01:00
parent a77053dc9e
commit a79bd85e14
1 changed files with 12 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
View File

@ -200,31 +200,26 @@ fun check_result_inv oid {is_monitor:bool} ctxt =
section\<open>Implementing Monitors\<close>
text\<open>
Since monitor-clauses have a regular expression syntax, it is natural
to implement them as deterministic automata. These are stored in the
\inlineisar+docobj_tab+ for monitor-objects in the \isadof component.
We implemented the functions:
Since monitor-clauses have a regular expression syntax, it is natural to implement them as
deterministic automata. These are stored in the \inlineisar+docobj_tab+ for monitor-objects
in the \isadof component. We implemented the functions:
\begin{sml}
val enabled : automaton -> env -> cid list
val next : automaton -> env -> cid -> automaton
\end{sml}
where \inlineisar+env+ is basically a map between internal automaton
states and class-id's (\inlineisar+cid+'s). An automaton is said to be
\emph{enabled} for a class-id, iff it either occurs in its accept-set
or its reject-set (see \autoref{sec:monitors}). During top-down
document validation, whenever a text-element is encountered, it is
checked if a monitor is \emph{enabled} for this class; in this case,
the \inlineisar+next+-operation is executed. The transformed automaton
recognizing the rest-language is stored in \inlineisar+docobj_tab+ if
possible; otherwise, if \inlineisar+next+ fails, an error is
reported. The automata implementation is, in large parts, generated
from a formalization of functional automata~\cite{Functional-Automata-AFP}.
where \inlineisar+env+ is basically a map between internal automaton states and class-id's
(\inlineisar+cid+'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id,
iff it either occurs in its accept-set or its reject-set (see @{docref "sec:monitors"}). During
top-down document validation, whenever a text-element is encountered, it is checked if a monitor
is \emph{enabled} for this class; in this case, the \inlineisar+next+-operation is executed. The
transformed automaton recognizing the rest-language is stored in \inlineisar+docobj_tab+ if
possible; otherwise, if \inlineisar+next+ fails, an error is reported. The automata implementation
is, in large parts, generated from a formalization of functional automata~\cite{Functional-Automata-AFP}.
\<close>
(*<*)
end
(*>*)