Commit 60327797 authored by Heiko Becker's avatar Heiko Becker

Fix HOL-Light conversions and some bugs in testcases

parent 25363795
(* First unfold all! definitions to the definitions known to the kernel
then remove all! conditionals using the conditional rewriting conversion
then get rid of all conditionals using NUM_REDUCE_CONV (TODO: What about equivalence of constants?)
then remove all let bindings
then simplify projections
then finally evaluate all rational functions until you arrive at true or false
*)
(* Define a list containing all defined functions, that need to be unfolded while evaluating *)
let Checker_Rewrites =
[CertificateChecker;validIntervalbounds; validErrorbound;
maxAbsFun; isSupersetInterval; multInterval; subtractInterval; widenInterval; mkInterval;
addInterval; absIntvUpd; min4; max4; machineEpsilon; IVlo; IVhi];;
(* Define a list containing only the distincness and injectivity properties, for simplifying conditionals *)
let DistinctnessAndInjectivity = [distinctness "exp"; injectivity "exp"; distinctness "binop"];;
(** Next two functions are based on suggestion from 2006 by John Harrison.
https://sourceforge.net/p/hol/mailman/message/2808187/
**)
(*
First get the free variables of the pattern
Then check wether the free variables can be instantiated such that pattern matches thm.
Since term_match may fail, check the returned instantiation on the pattern and check wether this is alpha convertibe (aconv) to the given thm.
If all this succeeds then return true, otherwise false
This version has been slightly modified, since the first argument to term_match are variables it should not instantiate...
*)
let matchable pat tm =
try aconv (instantiate(term_match (frees pat) pat tm) pat) tm
with Failure _ -> false;;
let matchable pattern term =
try
aconv (instantiate (term_match (frees term) pattern term) pattern) term
with
|Failure _ -> false;;
(*
test wether matchable pat tm is true.
If this holds true, then apply conv else recurse.
Recursion: If tm is a combination, recurse in the arguments, if tm is an abstraction, recurse into the term, commented out since it is not need in certificate checker
*)
let rec DEPTH_PAT_CONV pat (conv:term->thm) term =
if matchable pat term then conv else
match term with
Comb(s,t) -> COMB2_CONV (DEPTH_PAT_CONV pat conv s)
(DEPTH_PAT_CONV pat conv t)
(* | Abs(x,t) -> ABS_CONV (DEPTH_PAT_CONV pats t conv) *)
| _ -> REFL;;
(*
Subterm rewriting conversion
let REWRITE_SUBTERMS_CONV pats pat ths =
DEPTH_PAT_CONV pats pat (REWRITE_CONV(ADD_CLAUSES::MULT_CLAUSES::ths));;
Recursion: If tm is a combination, recurse in the arguments,
if tm is an abstraction, recurse into the term, commented out since it is not need in certificate checker
*)
let rec DEPTH_PAT_CONV pattern conv term :thm =
if (matchable pattern term)
then
conv term
else match term with
|Comb (s,t) -> COMB2_CONV (DEPTH_PAT_CONV pattern conv) (DEPTH_PAT_CONV pattern conv) term
|Abs (x,t) -> ABS_CONV (DEPTH_PAT_CONV pattern conv) term
|_ -> REFL term;;
(** OLD DAISY CONVERSION, NOT USED ANYMORE
let DAISY_CONV theRewrites term =
let allRewrites = List.concat [Checker_Rewrites; theRewrites; DistinctnessAndInjectivity] in
let unfolded_defs = REWRITE_CONV allRewrites term in
......@@ -69,94 +64,33 @@ let DAISY_CONV theRewrites term =
)
)
)
) no_lets;;
let matchable pattern term =
try
aconv (instantiate (term_match (frees term) pattern term) pattern) term
with
|Failure _ -> false;;
) no_lets;; **)
(** Benchmarking function, aply conversion to thm using CONV_RULE and compute time **)
let step conv t = time (CONV_RULE conv) t;;
let rec DEPTH_PAT_CONV pattern conv term :thm =
if (matchable pattern term)
then
conv term
else match term with
|Comb (s,t) -> COMB2_CONV (DEPTH_PAT_CONV pattern conv) (DEPTH_PAT_CONV pattern conv) term
|Abs (x,t) -> ABS_CONV (DEPTH_PAT_CONV pattern conv) term
|_ -> REFL term;;
let errsimp_conv = PATH_CONV "rr" (REWRITE_CONV theRewrites);;
let ivsimp_conv = PATH_CONV "rl" (REWRITE_CONV theRewrites);;
let unfold_defs_conv = PATH_CONV "r" (REWRITE_CONV Checker_Rewrites);;
let arith_conv =
(ONCE_DEPTH_CONV
(CHANGED_CONV
(TRY_CONV NUM_REDUCE_CONV THENC TRY_CONV REAL_RAT_RED_CONV)));;
let errorBound_conv =
(DEPTH_PAT_CONV `validErrorbound e E`
(ONCE_REWRITE_CONV [validErrorbound] THENC
DEPTH_CONV BETA_CONV THENC
COND_ELIM_CONV THENC
(*REWRITE_CONV [COND_ELIM_THM] THENC *)
REWRITE_CONV DistinctnessAndInjectivity THENC
(REPEATC (CHANGED_CONV (TRY_CONV (COND_ELIM_CONV THENC arith_conv)))) THENC
REPEATC let_CONV));;
let intervalBound_conv =
(DEPTH_PAT_CONV `validIntervalbounds e E P`
(ONCE_REWRITE_CONV [validIntervalbounds] THENC
DEPTH_CONV BETA_CONV THENC
REWRITE_CONV [COND_ELIM_THM] THENC
REWRITE_CONV DistinctnessAndInjectivity));;
let precond_conv =
(DEPTH_PAT_CONV `thePrecond n`
(ONCE_REWRITE_CONV [thePrecondition] THENC REWRITE_CONV[COND_ELIM_THM]));;
(** Simplifing conversions **)
let errsimp_conv rws = PATH_CONV "r" (REWRITE_CONV rws);;
let ivsimp_conv rws = PATH_CONV "l" (REWRITE_CONV rws);;
let unfold_defs_conv = REWRITE_CONV Checker_Rewrites;;
(** The versy same conversions for applications of conv_rule
TODO: Make this a PURE_REWRITE_CONV and benchmark
**)
let errsimp_convr rws = PATH_CONV "rr" (REWRITE_CONV rws);;
let ivsimp_convr rws = PATH_CONV "rl" (REWRITE_CONV rws);;
let unfold_defs_convr = PATH_CONV "r" (REWRITE_CONV Checker_Rewrites);;
(** Simple arithmetic conversions to evaluate arithmetic in Daisy certificates**)
let daisy_arith = (CHANGED_CONV (TRY_CONV NUM_REDUCE_CONV THENC TRY_CONV REAL_RAT_RED_CONV));;
let arith_conv = (ONCE_DEPTH_CONV daisy_arith);;
(* TODO: Test wether this can be simplified with DEPTH_CONV daisy_arith*)
let full_arith_conv = REPEATC (CHANGED_CONV arith_conv);;
let thm = REWRITE_CONV[CertificateChecker] term;;
let thm2 = step errsimp_conv thm;;
let thm3 = step (REPEATC (CHANGED_CONV errorBound_conv)) thm2;;
let thm5 = step ivsimp_conv thm3;;
let thm6 = step (REPEATC (CHANGED_CONV intervalBound_conv)) thm5;;
let thm8 = step unfold_defs_conv thm6;;
let thm9 = step precond_conv thm8;;
let thm10 = step full_arith_conv thm9;;
(* New stuff begins here *)
let test t = match t with |Comb(s,t) -> if (rator s = `COND`) then print_term s else print_term s;;
(test `COND c s t`);;
let rec ONCE_COND_CONDMANIP_CONV conv term =
match term with
|Abs (x,t) -> REFL term
|Var (x,t) -> REFL term
|Const (c,t) -> REFL term
|Comb(s,t) ->
if is_cond (term)
then (COMB2_CONV (COMB2_CONV (COMB2_CONV ALL_CONV conv) ALL_CONV) ALL_CONV) term
else
try CHANGED_CONV (COMB2_CONV (ONCE_COND_CONV conv) (ALL_CONV)) term with
|Failure _ ->
let _ = printf("Right-Hand") in
try (CHANGED_CONV (COMB2_CONV (ALL_CONV) (ONCE_COND_CONV conv))) term with Failure _ -> REFL term;;
(** Conversion that only applies to a conditional. Needed for final evaluation of certificate**)
let rec ONCE_COND_CONV conv term =
match term with
|Abs (x,t) -> REFL term
|Abs (x,t) -> ABS_CONV (ONCE_COND_CONV conv) term
|Var (x,t) -> REFL term
|Const (c,t) -> REFL term
|Comb(s,t) ->
......@@ -165,72 +99,55 @@ let rec ONCE_COND_CONV conv term =
else
try CHANGED_CONV (COMB2_CONV (ONCE_COND_CONV conv) (ALL_CONV)) term with
|Failure _ ->
let _ = printf("Right-Hand") in
try (CHANGED_CONV (COMB2_CONV (ALL_CONV) (ONCE_COND_CONV conv))) term with Failure _ -> REFL term;;
try (CHANGED_CONV (COMB2_CONV (ALL_CONV) (ONCE_COND_CONV conv))) term with
|Failure _ -> REFL term;;
(** Conversion to manipulate only the condition of the first encountered conditional**)
let ONCE_COND_MANIP_CONV conv = ONCE_COND_CONV (COMB2_CONV (COMB2_CONV (COMB2_CONV ALL_CONV conv) ALL_CONV) ALL_CONV);;
(ONCE_COND_CONDMANIP_CONV (REWRITE_CONV [ASSUME `(a:num) = b`]) THENC ONCE_COND_CONV (PURE_REWRITE_CONV[COND_CLAUSES])) `if (a:num) = b then a else b`;;
let COND_MANIP_CONV conv= (COMB2_CONV (COMB2_CONV (COMB2_CONV ALL_CONV conv) ALL_CONV) ALL_CONV);;
let matchable pattern term =
try
aconv (instantiate (term_match (frees term) pattern term) pattern) term
with
|Failure _ -> false;;
let step conv t = time (CONV_RULE conv) t;;
let rec DEPTH_PAT_CONV pattern conv term :thm =
if (matchable pattern term)
then
conv term
else match term with
|Comb (s,t) -> COMB2_CONV (DEPTH_PAT_CONV pattern conv) (DEPTH_PAT_CONV pattern conv) term
|Abs (x,t) -> ABS_CONV (DEPTH_PAT_CONV pattern conv) term
|_ -> REFL term;;
let errsimp_conv = PATH_CONV "rr" (REWRITE_CONV theRewrites);;
let ivsimp_conv = PATH_CONV "rl" (REWRITE_CONV theRewrites);;
let unfold_defs_conv = PATH_CONV "r" (REWRITE_CONV Checker_Rewrites);;
(* Now for conversion not for thm **)
let errsimp_conv = PATH_CONV "r" (REWRITE_CONV theRewrites);;
let ivsimp_conv = PATH_CONV "l" (REWRITE_CONV theRewrites);;
let unfold_defs_conv = REWRITE_CONV Checker_Rewrites;;
let arith_conv =
(ONCE_DEPTH_CONV
(CHANGED_CONV
(TRY_CONV NUM_REDUCE_CONV THENC TRY_CONV REAL_RAT_RED_CONV)));;
(ONCE_COND_MANIP_CONV (REWRITE_CONV [ASSUME `(a:num) = b`]) THENC ONCE_COND_CONV (PURE_REWRITE_CONV[COND_CLAUSES])) `if (a:num) = b then a else b`;;
(** Conversion to evaluate the errorBound part, apart from arithmetic **)
let errorBound_conv =
(DEPTH_PAT_CONV `validErrorbound e E`
(ONCE_REWRITE_CONV [validErrorbound] THENC
DEPTH_CONV BETA_CONV THENC
COND_ELIM_CONV THENC
(*ONCE_REWRITE_CONV [COND_ELIM_THM] THENC *)
REWRITE_CONV DistinctnessAndInjectivity THENC
REPEATC (CHANGED_CONV (ONCE_COND_CONV (COND_MANIP_CONV daisy_arith) THENC PURE_REWRITE_CONV[COND_CLAUSES])) THENC
(* COND_ELIM_CONV THENC
(*ONCE_REWRITE_CONV [COND_ELIM_THM] THENC *)
REWRITE_CONV DistinctnessAndInjectivity THENC *)
(REPEATC let_CONV)));;
(* (REPEATC
(CHANGED_CONV (
(TRY_CONV (COND_ELIM_CONV THENC REWRITE_CONV DistinctnessAndInjectivity THENC arith_conv)) THENC (REPEATC let_CONV))))));; *)
(** Conversion to evaluate the intervalBound part, apart from arithmetic **)
let intervalBound_conv =
(DEPTH_PAT_CONV `validIntervalbounds e E P`
(ONCE_REWRITE_CONV [validIntervalbounds] THENC
DEPTH_CONV BETA_CONV THENC
REWRITE_CONV [COND_ELIM_THM] THENC
REWRITE_CONV DistinctnessAndInjectivity));;
REWRITE_CONV DistinctnessAndInjectivity THENC
REPEATC (CHANGED_CONV (ONCE_COND_CONV (COND_MANIP_CONV daisy_arith) THENC PURE_REWRITE_CONV[COND_CLAUSES]))));;
let precond_conv =
let precond_conv P =
(DEPTH_PAT_CONV `thePrecondition n`
(ONCE_REWRITE_CONV [thePrecondition] THENC REWRITE_CONV[COND_ELIM_THM]));;
(ONCE_REWRITE_CONV [P] THENC REPEATC (CHANGED_CONV (ONCE_COND_CONV (COND_MANIP_CONV daisy_arith) THENC PURE_REWRITE_CONV[COND_CLAUSES]))));;
let full_arith_conv = REPEATC (CHANGED_CONV arith_conv);;
let DAISY_CONV checker precond rws =
REWRITE_CONV [checker] THENC
errsimp_conv rws THENC
(REPEATC (CHANGED_CONV errorBound_conv)) THENC
ivsimp_conv rws THENC
(REPEATC (CHANGED_CONV intervalBound_conv)) THENC
(precond_conv precond) THENC
unfold_defs_conv THENC
full_arith_conv;;
(**
(* Fast and easy *)
let thm = REWRITE_CONV[CertificateChecker] term;;
let thm2 = step errsimp_conv thm;;
(* First unfold the definitions for evaluation of the errorbound*)
let thm2 = step (errsimp_convr theRewrites) thm;;
let thm3 = step errorBound_conv thm2;;
......@@ -245,33 +162,15 @@ let thm7 = step errorBound_conv thm6;;
(** A test :Only 4.5 seconds! **)
let thm3_2 = step (REPEATC (CHANGED_CONV errorBound_conv)) thm2;;
let thm5 = step ivsimp_conv thm3_2;;
let thm5 = step (ivsimp_convr theRewrites) thm3_2;;
let thm6 = step (REPEATC (CHANGED_CONV intervalBound_conv)) thm5;;
let thm7 = step unfold_defs_conv thm6;;
let thm8 = step precond_conv thm7;;
let thm9 = step (DEPTH_PAT_CONV `if c then s else t` (REPEATC (CHANGED_CONV (DEPTH_CONV COND_ELIM_CONV THENC arith_conv)))) thm8;;
let thm8 = step (precond_conv thePrecondition) thm7;;
let thm10 = step (DEPTH_CONV (let_CONV)) thm9;;
let thm10 = step unfold_defs_convr thm9;;
let thm11 = step (REWRITE_CONV[FST; SND]) thm10;;
let thm12 = step full_arith_conv thm11;;
let DAISY_CONV =
REWRITE_CONV[CertificateChecker] THENC
errsimp_conv THENC
(REPEATC (CHANGED_CONV errorBound_conv)) THENC
ivsimp_conv THENC
(REPEATC (CHANGED_CONV intervalBound_conv)) THENC
unfold_defs_conv THENC
precond_conv THENC
(DEPTH_PAT_CONV `if c then s else t` (REPEATC (CHANGED_CONV (DEPTH_CONV COND_ELIM_CONV THENC arith_conv)))) THENC
(DEPTH_CONV let_CONV) THENC
REWRITE_CONV[FST; SND] THENC
full_arith_conv;;
let thm11 = step full_arith_conv thm10;;
let theThm = time DAISY_CONV term;;
let theThm = time (DAISY_CONV CertificateChecker thePrecondition theRewrites) term;;
**)
#!/bin/bash
####################################################################################
# #
# Experiments for CPP 2017 Paper. Run daisy on all testcases in the "formal" #
# directory. Then use the provers to get the runtimes and check the certificates #
# #
####################################################################################
#Configure a 20 minute stimeout for the HOL-Light scripts
TIMEOUT=20m
arr=()
while IFS= read -r -d $'\0'; do
arr+=("$REPLY")
done < <(find ./testcases/verification/ -name "*.scala" -print0)
mkdir -p ./coq/output
mkdir -p ./hol/output
done < <(find ./testcases/formal/ -name "*.scala" -print0)
for file in "${arr[@]}"
do
echo $file
echo "Coq certificate"
time (./daisy $file --certificate=coq >/dev/null)
## echo "Coq certificate"
## time (./daisy $file --certificate=coq >/dev/null)
echo "HOL Certificate"
time (./daisy $file --certificate=hol >/dev/null)
echo ""
done
#
#echo ""
#echo "[Certificate Test]"
#echo ""
echo ""
echo "[Certificate Test]"
echo ""
cd coq
arrCoq=()
while IFS= read -r -d $'\0'; do
arrCoq+=("$REPLY")
done < <(find ./output/ -name "*.v" -print0)
for file in "${arrCoq[@]}"
do
echo $file
echo ""
time (coqc -R ./ Daisy $file)
done
#cd coq
#arrCoq=()
#while IFS= read -r -d $'\0'; do
# arrCoq+=("$REPLY")
#done < <(find ./output/ -name "*.v" -print0)
#
#for file in "${arrCoq[@]}"
#do
# echo $file
# echo ""
# time (coqc -R ./ Daisy $file)
#done
cd ../hol
#cd ../hol
cd hol
arrHOL=()
while IFS= read -r -d $'\0'; do
......@@ -46,6 +54,11 @@ for file in "${arrHOL[@]}"
do
echo $file
echo ""
time ((ocaml < $file) &>.$file)
timeout $TIMEOUT time ocaml<$file &>.$file
RETVAL=$?
if [ $RETVAL -eq 124 ]
then echo "TIMEOUT "$file
else echo "SUCCESS "$file
fi
done
......@@ -396,7 +396,7 @@ object CertificatePhase extends DaisyPhase {
if (prover == "coq")
"Eval compute in CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "."
else
"DAISY_CONV theRewrites `CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "`;;"
"DAISY_CONV CertificateChecker thePrecondition theRewrites `CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "`;;"
private def getAllComputeExps (e:Expr, analysisResultName:String,precondName:String, prover:String) :String=
{
......@@ -429,7 +429,7 @@ object CertificatePhase extends DaisyPhase {
}
}
else
"DAISY_CONV theRewrites `CertificateChecker " + nameE + " " + analysisResultName + " " + precondName + "`;;"
"DAISY_CONV CertificateChecker thePrecondition theRewrites `CertificateChecker " + nameE + " " + analysisResultName + " " + precondName + "`;;"
}
private def holExpList (e:Expr) :String =
......
......@@ -4,9 +4,9 @@ import daisy.lang._
import Real._
object Doppler {
object AdditionSimple {
def doppler(u: Real): Real = {
def additionSimple(u: Real): Real = {
require(-100.0 <= u && u <= 100)
331.4 + u
......
import daisy.lang._
import Real._
object InvertedPendulum4 {
// all: <1, 32, 30> [-1, 1]
def out1() = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1)
(1.536200) * s1 + (2.025400) * s2 + (-16.519200) * s3 + (-2.735800) * s4
}
def state1() = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1 &&
-1 <= y1 && y1 <= 1 && -1 <= y2 && y2 <= 1)
(0.998301) * s1 + (0.001002) * s2 + (-0.000114) * s3 + (-0.000002) * s4 + (0.001700) * y1 + (0.000100) * y2
}
def state2() = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1 &&
-1 <= y1 && y1 <= 1 && -1 <= y2 && y2 <= 1)
(0.000693) * s1 + (1.003500) * s2 + (-0.029160) * s3 + (-0.004972) * s4 + (0.002100) * y1 + (0.001800) * y2
}
def state3() = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1 &&
-1 <= y1 && y1 <= 1 && -1 <= y2 && y2 <= 1)
(-0.001197) * s1 + (0.000004) * s2 + (0.987778) * s3 + (0.000994) * s4 + (0.001200) * y1 + (0.012200) * y2
}
def state4() = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= s4 && s4 <= 1 &&
-1 <= y1 && y1 <= 1 && -1 <= y2 && y2 <= 1)
(0.006982) * s1 + (0.008751) * s2 + (-0.120899) * s3 + (0.987581) * s4 + (0.000000) * y1 + (0.077000) * y2
}
}
\ No newline at end of file
......@@ -4,9 +4,9 @@ import daisy.lang._
import Real._
object Doppler {
object MultiplicationSimple {
def doppler(u: Real): Real = {
def multiplicationSimple(u: Real): Real = {
require(-100.0 <= u && u <= 100)
100 * u
......
......@@ -4,9 +4,9 @@ import daisy.lang._
import Real._
object Doppler {
object MultiplicationSimple2 {
def doppler(u: Real): Real = {
def multiplicationSimple2(u: Real): Real = {
require(-100.0 <= u && u <= 100)
331.4 * u
......
......@@ -5,24 +5,24 @@ import Real._
object Pitch {
// s1, s2, s3, y1: <1, 32, 30>, [-1, 1]
def out1(s1: Real, s2: Real, s3: Real) = {
def out1(s1: Real, s2: Real, s3: Real): Real = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1)
(0.120200) * state1 + (-42.565500) * state2 + (-1.000100) * state3
}
def state1(s1: Real, s2: Real, s3: Real, y1: Real) = {
def state1(s1: Real, s2: Real, s3: Real, y1: Real): Real = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1)
(0.999715) * state1 + (0.046781) * state2 + (-0.000333) * state3 + (0.000100) * y1
}
def state2(s1: Real, s2: Real, s3: Real, y1: Real) = {
def state2(s1: Real, s2: Real, s3: Real, y1: Real): Real = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1)
(-0.000011) * state1 + (0.998710) * state2 + (-0.000020) * state3 + (0.000000) * y1
}
def state3(s1: Real, s2: Real, s3: Real, y1: Real) = {
def state3(s1: Real, s2: Real, s3: Real, y1: Real): Real = {
require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= s3 && s3 <= 1 && -1 <= y1 && y1 <= 1)
(-0.000000) * state1 + (0.056663) * state2 + (0.998299) * state3 + (0.001700) * y1
}
}
\ No newline at end of file
}
import daisy.lang._
import Real._
object RigidBody {
//x1, x2, x3: < 1, 16 11>, [-15, 15]
def out1(x1: Real, x2: Real, x3: Real): Real = {
require(-15 <= x1 && x1 <= 15 && -15 <= x2 && x2 <= 15 && -15 <= x3 && x3 <= 15)
-x1*x2 - 2*x2*x3 - x1 - x3
}
// apparently this needs 17 bits, or we've not been accurate enough
def out2(x1: Real, x2: Real, x3: Real): Real = {
require(-15 <= x1 && x1 <= 15 && -15 <= x2 && x2 <= 15 && -15 <= x3 && x3 <= 15)
2*x1*x2*x3 + 3*x3*x3 - x2*x1*x2*x3 + 3*x3*x3 - x2
}
}
\ No newline at end of file
......@@ -4,9 +4,9 @@ import daisy.lang._
import Real._
object Doppler {
object SubtractionSimple {
def doppler(u: Real): Real = {
def SubtractionSimple(u: Real): Real = {
require(-100.0 <= u && u <= 100)
331.4 - u
......
......@@ -4,9 +4,9 @@ import daisy.lang._
import Real._
object Doppler {
object SubtractionSimple2 {
def doppler(u: Real): Real = {
def subtractionSimple2(u: Real): Real = {
require(-100.0 <= u && u <= 100)
(- 331.4) - u
......
import daisy.lang._
import Real._
object Traincar4 {
def state1(s0: Real, s1: Real) = {
require(-2.5 <= s0 && s0 <= 6.5 && -2.5 <= s1 && s1 <= 6.5)
s0 + (-9.6239E-08)*s1 }
}
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