ProB now supports the Atelier-B datatypes REAL and FLOAT. You can turn off this support via the preference ALLOW_REALS.
Standard arithmetic operators can be applied to reals: +, - , *, /, SIGMA, PI.
Exponentiation of a real with an integer is also allowed.
The comparison predicates =, /=, <, >, <=, >= also all work.
Support for reals and floats is experimental. The definition in Atelier-B is also not stable yet. Currently ProB supports floating point numbers only. Warning: properties such as associativity and commutativity of arithmetic operators thus does not hold.
The library LibraryReals.def in stdlib contains additional useful External Functions (like RSIN, RCOS, RLOG, RSQRT, RPOW, ...).
Here is an example which uses the new datatype both in the modelling and in the VisB visualization:
MACHINE WaterTank_v3
// see https://www.ariadne-cps.org/tutorial/
// assuming continuous opening/closing
// Solution for aperture closed:
// y' = 0.3 - 0.02 y
// y(x) = c_1 e^(-0.02 x) + 15
// Solution for aperture open:
// y' = - 0.02 y
// y(x) = c_1 e^(-0.02 x)
// Parameterised solution for aperture open parameter a:0..1:
// y'(x) = 0.3 a - 0.02 y(x)
// y(x) = 15 a + c_1 e^(-0.02 x)
// Solution for a=1/T
// y' = 0.3(1/y) - 0.02 y
// y(x) = -sqrt(2.71828^(2 c_1 - 0.04 x) + 15)
DEFINITIONS
"LibraryReals.def";
"LibraryStrings.def";
VISB_JSON_FILE == "";
VISB_SVG_FILE == "";
MARGIN == 50.0;
VISB_SVG_CONTENTS == '''<defs>
<linearGradient id=\"grad_ok\" x1=\"0%\" y1=\"0%\" x2=\"0%\" y2=\"100%\">
<stop offset=\"0%\" style=\"stop-color:rgb(0,0,255);stop-opacity:1\" />
<stop offset=\"100%\" style=\"stop-color:rgb(90,10,205);stop-opacity:1\" />
</linearGradient>
<linearGradient id=\"grad_red\" x1=\"0%\" y1=\"0%\" x2=\"0%\" y2=\"100%\">
<stop offset=\"0%\" style=\"stop-color:rgb(255,0,0);stop-opacity:1\" />
<stop offset=\"100%\" style=\"stop-color:rgb(90,10,205);stop-opacity:1\" />
</linearGradient>
</defs>''';
VISB_SVG_BOX == rec(height:400, width:500,
viewBox: "4 0 16 10");
MAXL == 5; // maximum level for tank
level2yr(lvl) == 7.0 - lvl;
level2yi(lvl) == 7 - lvl;
VISB_SVG_OBJECTS1 == rec(`id`:"tank", svg_class:"rect", stroke:"none",
x:5, width:10,
y:level2yr(level), height:level,
fill: IF level>hmax or level<hmin THEN "url(#grad_red)" ELSE "url(#grad_ok)" END);
VISB_SVG_OBJECTS2 == rec(`id`:"outline", svg_class:"rect", stroke:"black",
`stroke-width`:0.1,
x:5, width:10, y:level2yi(MAXL), height:MAXL, fill:"none");
VISB_SVG_OBJECTS3 == {tick,h•tick:0..MAXL & h=IF tick mod 5=0 THEN 0.2 ELSE 0.2 END|
rec(`id`:("tick",tick), svg_class:"line", stroke:"black",
`stroke-width`:0.1,
y1:level2yi(tick), y2:level2yi(tick), x1:15.0, x2:15.0+h)};
VISB_SVG_OBJECTS4 == {tick•tick:{hmin,hmax}|
rec(`id`:("sensor",tick), svg_class:"line", stroke:"red",
`stroke-width`:0.1,
y1:level2yr(tick), y2:level2yr(tick), x1:4.4, x2:5.0)};
VISB_SVG_OBJECTS5 == {tick•tick:{hmin+δ,hmax-δ}|
rec(`id`:("sensor",tick), svg_class:"line", stroke:"gray",
`stroke-width`:0.1,
y1:level2yr(tick), y2:level2yr(tick), x1:4.6, x2:5.0)};
VISB_SVG_OBJECTS6 == rec(`id`:"valve", svg_class:"rect", stroke:"none",
x:9.90-a/2.0, width:a+0.2,
y:real(level2yi(MAXL))-1.25, height:1.25,
fill: IF valve=closed THEN "black"
ELSIF valve=closing THEN "cadetblue"
ELSIF valve=opening THEN "cornflowerblue"
ELSE "url(#grad_ok)" END);
//STEPSIZES == {1.0, 0.1, 0.01};
STEPSIZES == {1.0} // Stepsizes for continuous events below
SETS
ValveStatus = {opened,closed,opening,closing}
CONSTANTS
hmin /*@desc "minimum safe water level" */,
hmax /*@desc "maximum safe water level" */,
δ /*@desc "safety margin of sensors" */,
closingTime
PROPERTIES
hmin = 2.0 &
hmax = 4.0 &
δ = 0.5 &
closingTime = 4.0
VARIABLES
level /*@desc "Water level of the watertank" */,
valve /*@desc "valve status for inflowing water; if valve closed water level decreases" */,
a /*@desc "Aperture of valve" */
INVARIANT
/*@label "SAF-1" */ level >= hmin &
/*@label "SAF-2" */ level <= hmax &
valve: ValveStatus &
a:REAL & a>=0.0 & a<=1.0 &
(valve=closed => a=0.0) &
(valve=opened => a=1.0)
INITIALISATION
level:=(hmin+hmax) / 2.0 || valve := closed || a:= 0.0
OPERATIONS
// CONTINUOUS EVENTS; with TIME STEP PARAMETER δT
FlowConstantValveAperture(δT,c1) =
// in this case the aperture remains constant: below we get a precise solution of the differential equaion
SELECT
valve : {opened,closed} /*@desc "the aperture is fixed at the moment" */ &
δT : STEPSIZES &
c1 = level - 15.0*a /*@desc "determine constant c1 of diff. eq. solution" */ &
(valve=closed => level > hmin) /*@desc "we do not trigger ValveCanOpen" */ &
(valve=opened => level < hmax) /*@desc "we do not trigger ValveCanClose" */
// we could check that new level value is in bounds as well
// currently the event allows to overshoot hmax-δ or undershoot hmin+δ
THEN
level := c1 * REXP(-0.02 * δT) + 15.0*a
END;
FlowOpeningValve(δT,c1) =
// in this case the aperture is increasing; below is not a precise solution
SELECT
valve : {opening} /*@desc "the aperture is increasing at the moment" */ &
a < 1.0 /*@desc "not yet fully opened" */ &
δT : STEPSIZES &
c1 = level - 15.0*a /*@desc "determine constant c1 of diff. eq. solution (assuming fixed a)" */
THEN
level := c1 * REXP(-0.02 * δT) + 15.0*a ||
a := min({a + δT/closingTime,1.0})
END;
FlowClosingValve(δT,c1) =
// in this case the aperture is decreasing; below is not a precise solution
SELECT
valve : {closing} /*@desc "the aperture is decreasing at the moment" */ &
a > 0.0 /*@desc "not yet fully closed" */ &
δT : STEPSIZES &
c1 = level - 15.0*a /*@desc "determine constant c1 of diff. eq. solution (assuming fixed a)" */
THEN
level := c1 * REXP(-0.02 * δT) + 15.0*a ||
a := max({a - δT/closingTime,0.0})
END;
// Internal Discrete Events, occurring when valve closing/opening finished:
ValveClosed = SELECT valve=closing & a=0.0 THEN
valve := closed
END;
ValveOpened = SELECT valve=opening & a=1.0 THEN
valve := opened
END;
// Discrete Controller Events:
ValveCanClose = SELECT level >= hmax - δ & valve:{opened,opening} THEN
valve := closing
END;
ValveCanOpen = SELECT level <= hmin + δ & valve:{closed,closing} THEN
valve := opening
END
END