diff --git a/Reals/WaterTankReals.tla b/Reals/WaterTankReals.tla index 7ef24def8e8633529bc290068d33f7d9d436e551..47318f74d0e522c4fb199573daab0f20c793dc80 100644 --- a/Reals/WaterTankReals.tla +++ b/Reals/WaterTankReals.tla @@ -29,7 +29,8 @@ maxw == high_threshold+inflow \* maximum capacity as shown Invariant == level > 0.0 /\ level <= maxw convy(lvl) == bot-lvl VISB_SVG_BOX == [width |-> wid+4.0*lft, height |-> bot+lft] -VISB_SVG_OBJECTS0 == [svg_class |-> "rect", x|->lft, y |-> convy(level), height |-> level, width |-> wid, +VISB_SVG_OBJECTS0 == [svg_class |-> "rect", x|->lft, y |-> convy(level), +height |-> level, width |-> wid, fill |-> "lightsteelblue"] VISB_SVG_OBJECTS1 == [svg_class |-> "rect", x|->lft, y |-> convy(maxw), height |-> maxw, width |-> wid, fill |-> "none", stroke |-> "black", stroke_width|->1.0] @@ -44,6 +45,7 @@ VISB_SVG_OBJECTS4 == [svg_class |-> "rect", x|->lft, y |-> 2.0*lft, height |-> l stroke |-> "black", stroke_width|->1.0] VISB_SVG_OBJECTS5 == [svg_class |-> "text", x|->lft+5.0, y |-> 2.0*lft-8.0, text|->"Pump:", font_size|->8.0] VISB_SVG_OBJECTS6 == [svg_class |-> "text", x|->lft+9.5, y |-> 2.0*lft+7.2, text|->IF pump THEN "on" ELSE "off", font_size|->8.0] + -------------------------------------------------------------- THEOREM WaterTank => []Init ============================================================== \ No newline at end of file