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