Commit a495714e authored by Heiko Becker's avatar Heiko Becker
Browse files

Prepare everything to run proper timing experiments, by making HOL Light...

Prepare everything to run proper timing experiments, by making HOL Light scripts exit after execution
parent caa156c7
......@@ -7,20 +7,6 @@ done < <(find ./testcases/verification/ -name "*.scala" -print0)
mkdir -p ./coq/output
mkdir -p ./hol/output
#declare -a arr=("testcases/verification/control_BatchReactor.scala" \
#"testcases/verification/control_BatchProcessor.scala" \
#"testcases/verification/control_BallBeam.scala" \
#"testcases/verification/control_Bicycle.scala" \
#"testcases/verification/control_DCMotor.scala" \
#"testcases/verification/control_InvertedPendulum.scala" \
#"testcases/verification/control_InvertedPendulum4.scala" \
#"testcases/verification/control_Pitch.scala" \
#"testcases/verification/control_RigidBody.scala" \
#"testcases/verification/control_Traincar1.scala" \
#"testcases/verification/control_Traincar2.scala" \
#"testcases/verification/control_Traincar3.scala" \
#"testcases/verification/control_Traincar4.scala" \
#)
for file in "${arr[@]}"
do
......@@ -29,6 +15,7 @@ do
time (./daisy $file --certificate=coq >/dev/null)
echo "HOL Certificate"
time (./daisy $file --certificate=hol >/dev/null)
echo ""
done
echo ""
......@@ -59,6 +46,6 @@ for file in "${arrHOL[@]}"
do
echo $file
echo ""
time ((ocaml < $file) &>/dev/null)
time ((ocaml < $file) &>../output/log_$file)
done
......@@ -54,15 +54,15 @@ object CertificatePhase extends DaisyPhase {
//the analysis result function
val (analysisResultText, analysisResultName) = getAbsEnvDef(theBody.get, prv)
//generate the final evaluation statement
//val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,prv)
val functionCall = getAllComputeExps(theBody.get, analysisResultName, functionName, prv)
val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,prv)
//val functionCall = getAllComputeExps(theBody.get, analysisResultName, functionName, prv)
//compose the strings
val textWithoutFCall = prelude + "\n\n" + theDefinitions + "\n\n" + thePreconditionFunction + "\n" + analysisResultText
val certificateText =
if (prv == "coq")
textWithoutFCall + "\n\n" + functionCall
else
textWithoutFCall + "let theRewrites = [thePrecondition;absenv;" + holExpList(theBody.get) + "];;" + "\n" + functionCall
textWithoutFCall + "let theRewrites = [thePrecondition;absenv;" + holExpList(theBody.get) + "];;" + "\n" + functionCall + "\nexit(0);;"
//write to the output file
writeToFile(certificateText,prv,fnc.id.toString)
......
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