No edit summary |
No edit summary |
||

Line 6: | Line 6: | ||

Exponentiation of a real with an integer is also allowed. | Exponentiation of a real with an integer is also allowed. | ||

The comparison predicates =, /=, <, >, <=, >= also all work. | The comparison predicates =, /=, <, >, <=, >= also all work. | ||

There are also three conversion functions: | |||

* floor | |||

* ceiling | |||

* real | |||

Literals in decimal notation are supported. | |||

Support for reals and floats is still being improved. | Support for reals and floats is still being continuously improved. | ||

Currently ProB supports floating point numbers only. | Currently ProB supports floating point numbers only. | ||

Warning: properties such as associativity and commutativity of arithmetic operators | Warning: properties such as associativity and commutativity of arithmetic operators |

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.

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 // 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