• Special Pages
• User

Help

Reals and Floats: Difference between revisions

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, min, max. Exponentiation of a real with an integer is also allowed. The comparison predicates =, /=, <, >, <=, >= also all work. There are also three conversion functions:

• floor
• ceiling
• real

Literals in decimal notation are supported. Note that there is no automatic conversion from real to integer or the other way around. Hence 2*1.0 is a type error but you can write either real(2)*1.0 or 2*floor(1.0) or 2*ceiling(1.0)

Support for reals and floats is still being continuously improved. Currently ProB supports floating point numbers only. Warning: properties such as associativity and commutativity of arithmetic operators thus does not hold. In future we may provide a different internal representation for reals and floats and provide proper constraint solving. The definition in Atelier-B may also not be stable yet.

The library LibraryReals.def in stdlib contains additional useful External Functions:

• trigonometric functions like RSIN, RCOS, RTAN, RCOT, RSINH, ... and conversion functions RADIANS, DEGREE
• square root RSQRT
• logarithms and exponenation: RLOG, RLOGe, RPOW,
• constants REULER, RPI, RZERO, RONE
• other utilities: RSIGN, RABS, RFRACTION, ROUND
• comparison predicates RLEQ, RGEQ, RLT, RGT, REQ, RNEQ

Here is an example which uses the new datatype both in the modelling and in the VisB visualization:

```MACHINE WaterTank_v3
// assuming continuous opening/closing
// B model by Michael Leuschel, Dec. 2023

// 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>
<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\" />
<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\" />
</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"
//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
```