Skip to content
Snippets Groups Projects
Commit 824f9722 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

minor change

parent 9cb30130
No related branches found
No related tags found
No related merge requests found
...@@ -29,7 +29,8 @@ maxw == high_threshold+inflow \* maximum capacity as shown ...@@ -29,7 +29,8 @@ maxw == high_threshold+inflow \* maximum capacity as shown
Invariant == level > 0.0 /\ level <= maxw Invariant == level > 0.0 /\ level <= maxw
convy(lvl) == bot-lvl convy(lvl) == bot-lvl
VISB_SVG_BOX == [width |-> wid+4.0*lft, height |-> bot+lft] 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"] fill |-> "lightsteelblue"]
VISB_SVG_OBJECTS1 == [svg_class |-> "rect", x|->lft, y |-> convy(maxw), height |-> maxw, width |-> wid, VISB_SVG_OBJECTS1 == [svg_class |-> "rect", x|->lft, y |-> convy(maxw), height |-> maxw, width |-> wid,
fill |-> "none", stroke |-> "black", stroke_width|->1.0] 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 ...@@ -44,6 +45,7 @@ VISB_SVG_OBJECTS4 == [svg_class |-> "rect", x|->lft, y |-> 2.0*lft, height |-> l
stroke |-> "black", stroke_width|->1.0] 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_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] 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 THEOREM WaterTank => []Init
============================================================== ==============================================================
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment