Commit bba3ec21 authored by Claudio Gomes's avatar Claudio Gomes
Browse files

fix problem with vdm

parent c702f332
...@@ -7,6 +7,11 @@ instance variables ...@@ -7,6 +7,11 @@ instance variables
steeringActuator : SteeringActuator; steeringActuator : SteeringActuator;
kpPort : RealPort; kpPort : RealPort;
values
math: MATH = new MATH()
operations operations
public Controller : RealPort * PositionSensor * SteeringActuator ==> Controller public Controller : RealPort * PositionSensor * SteeringActuator ==> Controller
...@@ -27,7 +32,7 @@ loop()== ...@@ -27,7 +32,7 @@ loop()==
let beta : real = positionSensor.getBeta() let beta : real = positionSensor.getBeta()
in in
( (
steeringActuator.setSteering(-kp*y); steeringActuator.setSteering(math.sin(-kp*y));
); );
) )
......
class MATH
-- Overture STANDARD LIBRARY: MATH
-- --------------------------------------------
-- Version 1.0.0
--
-- Standard library for the Overture Interpreter. When the interpreter
-- evaluates the preliminary functions/operations in this file,
-- corresponding internal functions is called instead of issuing a run
-- time error. Signatures should not be changed, as well as name of
-- module (VDM-SL) or class (VDM++). Pre/post conditions is
-- fully user customisable.
-- Dont care's may NOT be used in the parameter lists.
functions
public static
sin:real +> real
sin(v) ==
is not yet specified
post abs RESULT <= 1;
public static
cos:real +> real
cos(v) ==
is not yet specified
post abs RESULT <= 1;
public static
tan:real -> real
tan(a) ==
is not yet specified
pre cos(a) <> 0;
public static
cot:real -> real
cot(a) ==
is not yet specified -- Could also be: 1/tan(r)
pre sin(a) <> 0;
public static
asin:real -> real
asin(a) ==
is not yet specified
pre abs a <= 1;
public static
acos:real -> real
acos(a) ==
is not yet specified
pre abs a <= 1;
public static
atan:real +> real
atan(v) ==
is not yet specified;
public static
acot:real +> real
acot(a) ==
atan(1/a)
pre a <> 0;
public static
sqrt:real -> real
sqrt(a) ==
is not yet specified
pre a >= 0;
public static
pi_f:() +> real
pi_f () ==
is not yet specified
operations
public static
srand:int ==> ()
srand(a) ==
let - = MATH`srand2(a) in skip
pre a >= -1;
public static
rand:int ==> int
rand(a) ==
is not yet specified;
public static
srand2:int ==> int
srand2(a) ==
is not yet specified
pre a >= -1
functions
public static
exp:real +> real
exp(a) ==
is not yet specified;
public static
ln:real -> real
ln(a) ==
is not yet specified
pre a > 0;
public static
log:real -> real
log(a) ==
is not yet specified
pre a > 0;
public static
fac:nat -> nat1
fac(a) ==
is not yet specified
pre a < 21; -- The limit for 64-bit calculations
values
public
pi = 3.14159265358979323846
end MATH
Supports Markdown
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