Commit d8156d37 authored by Markus Klinik's avatar Markus Klinik
Browse files

plan relaxation

parent a9c83bd4
......@@ -195,3 +195,7 @@ Given the step function and the IUT, Gast generates lists of actions of increasi
It feeds each list to both the model and the IUT, and compares their outputs.
The IUT always returns \false, while the model returns \false\ until the goal predicate is satisfied.
Once the goal predicate is satisfied, Gast thinks that it found a counterexample and reports the list of actions that leads to the differing output.
This counterexample is a valid plan.
\subsection{Plan Relaxation Using Dependence Analysis}
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