doc-src/TutorialI/CTL/ctl.tex
author blanchet
Sat, 07 Mar 2009 16:47:36 +0100
changeset 30349 110826d1e5ff
parent 11458 09a6c44a48ea
child 48522 708278fc2dff
permissions -rw-r--r--
Added a second timeout mechanism to Refute. For some reason, TimeLimit.timeLimit often does not work, and it leaves Refute running forever, making any evaluation using Mutabelle or Mirabelle impossible. The redundant timeout seems to do the trick.

\index{model checking example|(}%
\index{lfp@{\texttt{lfp}}!applications of|see{CTL}}
\input{CTL/document/Base.tex}
\input{CTL/document/PDL.tex}
\input{CTL/document/CTL.tex}
\index{model checking example|)}