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