Commit 630b8d50 authored by MARCHE Claude's avatar MARCHE Claude

some ideas for the smoke detector

parent 307fc8af
......@@ -85,10 +85,15 @@
- also: BTS 13736
https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* Smoke detector and absurd: on pourrait mettre un label particulier
sur le "false" genéré par absurd, pour indiquer que c'est
intentionel que l'on veuille prouver false. Un tel cas pourrait etre
traité de facon speciale par le smoke detector avec option "deep",
pour eviter une fausse alarme.
* Documentation
- (ANDREI) make the glossary available
- (CLAUDE) revoir documentation du smoke detector
- DONE (CLAUDE) revoir documentation du smoke detector
- (CLAUDE) complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
......@@ -102,6 +107,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* deplacer option -bench de why3replayer dans une commande de why3session
* IDE
** todo: run detection immediately at start up if conf file absent or
outdated. should become doable with the new Session module
......
......@@ -463,37 +463,49 @@ option \verb|-force| described below.
\paragraph{Smoke Detector}
The smoke detector tries to detect if the context is self-contradicting
and, thus, that anything can be proved in this context. The smoke
detector can't be run on outdated session and does not modify the session.
It has three possible configurations:
\begin{itemize}
The smoke detector tries to detect if the context is
self-contradicting and, thus, that anything can be proved in this
context. The smoke detector can't be run on an outdated session and does
not modify the session. It has three possible configurations:
\begin{itemize}
\item \texttt{none}: Do not run the smoke detector.
\item \texttt{top}: The negation of each proved goal is sent with the
same timeout to the prover that proved the original goal.
same timeout to the prover that proved the original goal.
\begin{verbatim}
Goal G : forall x:int. q x -> (p1 x \/ p2 x)
Goal G : forall x:int. q x -> (p1 x \/ p2 x)
\end{verbatim}
becomes
becomes
\begin{verbatim}
Goal G : ~ (forall x:int. q x -> (p1 x \/ p2 x))
Goal G : ~ (forall x:int. q x -> (p1 x \/ p2 x))
\end{verbatim}
\item \texttt{deep}: This is the same technique as \texttt{top} but the
negation is pushed under the universal quantification (without
changing them) and under the implication. The previous example becomes
In other words, if the smoke detector is triggered, it means that the context
of the goal \texttt{G} is self-contradicting.
\item \texttt{deep}: This is the same technique as \texttt{top} but
the negation is pushed under the universal quantification (without
changing them) and under the implication. The previous example
becomes
\begin{verbatim}
Goal G : forall x:int. q x /\ ~ (p1 x \/ p2 x)
Goal G : forall x:int. q x /\ ~ (p1 x \/ p2 x)
\end{verbatim}
\end{itemize}
In other words, the premises of goal \texttt{G} are pushed in the
context, so that if the smoke detector is triggered, it means that
the context of the goal \texttt{G} and its premises are
self-contradicting. It should be clear that detecting smoke in that
case does not necessarily means that there is a mistake: for
example, this could occur in the WP of a program with an infeasible
path.
\end{itemize}
\noindent
The name of the goals that triggered the smoke detector are printed:
At the end of the replay, the name of the goals that triggered the
smoke detector are printed:
\begin{verbatim}
goal 'G', prover 'Alt-Ergo 0.93.1': Smoke detected!!!
goal 'G', prover 'Alt-Ergo 0.93.1': Smoke detected!!!
\end{verbatim}
Moreover \texttt{Smoke detected} (exit code 1) is printed at the end if the smoke
detector has been triggered, or \texttt{No smoke detected} (exit code 0)
otherwise.
Moreover \texttt{Smoke detected} (exit code 1) is printed at the end
if the smoke detector has been triggered, or \texttt{No smoke
detected} (exit code 0) otherwise.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment