diff --git a/Lift/Lift.mch b/Lift/Lift.mch new file mode 100644 index 0000000000000000000000000000000000000000..2dd88119b6061d41a524b420dfd448faf2420685 --- /dev/null +++ b/Lift/Lift.mch @@ -0,0 +1,50 @@ +MACHINE Lift +/* A simple model of a lift without a controller; The controller + will be added in a refinement (by refining the lift moving operations) or + by a CSP controller */ +DEFINITIONS + FLOORS == (groundf .. topf); + all_buttons_pressed == (inside_buttons \/ call_buttons); + /* Note: one could make a slightly simpler spec by only keeping a single all_buttons_pressed variable */ + ASSERT_LTL == "G ([push_call_button(groundf)] -> X F {cur_floor=groundf & door_open=TRUE})"; + ASSERT_LTL2 == "G ([push_inside_button(topf)] -> X F {cur_floor=topf & door_open=TRUE})" + /* These LTL properties are violated: e.g., the machine can reverse infinitely without moving */ +CONSTANTS groundf,topf +PROPERTIES + groundf:INT & topf:INT & groundf < topf +VARIABLES cur_floor, inside_buttons, door_open, call_buttons,direction_up +INVARIANT + cur_floor : FLOORS & + inside_buttons <: FLOORS & + door_open : BOOL & + call_buttons <: FLOORS & + direction_up : BOOL +INITIALISATION + cur_floor := groundf || inside_buttons := {} || door_open := FALSE || call_buttons := {} || direction_up := TRUE +OPERATIONS + /* The lift operations : */ + move_up = PRE door_open = FALSE & cur_floor <topf & direction_up=TRUE THEN + cur_floor := cur_floor +1 + END; + move_down = PRE door_open = FALSE & cur_floor>groundf & direction_up=FALSE THEN + cur_floor := cur_floor - 1 + END; + reverse_lift_down = PRE direction_up=TRUE THEN direction_up := FALSE END; + reverse_lift_up = PRE direction_up=FALSE THEN direction_up := TRUE END; + open_door = PRE door_open = FALSE & cur_floor : all_buttons_pressed THEN + door_open := TRUE + END; + close_door = PRE door_open = TRUE THEN + door_open := FALSE || + /* clear requests as floor now visited: */ + inside_buttons := inside_buttons - {cur_floor} || call_buttons := call_buttons - {cur_floor} + END; + + /* The user interface : */ + push_inside_button(b) = PRE b:FLOORS & b/: inside_buttons & b/=cur_floor THEN + inside_buttons := inside_buttons \/ {b} + END; + push_call_button(b) = PRE b:FLOORS & b/: call_buttons THEN + call_buttons := call_buttons \/ {b} + END +END \ No newline at end of file diff --git a/Lift/lift.json b/Lift/lift.json new file mode 100644 index 0000000000000000000000000000000000000000..28d19a986a381d20871c757ed3fe2ed35697d2d4 --- /dev/null +++ b/Lift/lift.json @@ -0,0 +1,267 @@ +{ + "svg":"lift.svg", + "items":[ + { + "id":"floor_2", + "attr":"visibility", + "value":"IF topf=2 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"floor_1", + "attr":"visibility", + "value":"IF topf:{1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"floor_0", + "attr":"visibility", + "value":"IF topf:{0,1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"floor_U", + "attr":"visibility", + "value":"IF groundf=-1 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"text_2", + "attr":"visibility", + "value":"IF topf=2 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"text_1", + "attr":"visibility", + "value":"IF topf:{1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"text_0", + "attr":"visibility", + "value":"IF topf:{0,1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"text_U", + "attr":"visibility", + "value":"IF groundf=-1 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"inside_text_2", + "attr":"visibility", + "value":"IF topf=2 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"inside_text_1", + "attr":"visibility", + "value":"IF topf:{1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"inside_text_0", + "attr":"visibility", + "value":"IF topf:{0,1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"inside_text_U", + "attr":"visibility", + "value":"IF groundf=-1 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"button_2", + "attr":"visibility", + "value":"IF topf=2 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"button_1", + "attr":"visibility", + "value":"IF topf:{1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"button_0", + "attr":"visibility", + "value":"IF topf:{0,1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"button_U", + "attr":"visibility", + "value":"IF groundf=-1 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"inside_2", + "attr":"visibility", + "value":"IF topf=2 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"inside_1", + "attr":"visibility", + "value":"IF topf:{1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"inside_0", + "attr":"visibility", + "value":"IF topf:{0,1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"inside_U", + "attr":"visibility", + "value":"IF groundf=-1 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"lift", + "attr":"fill", + "value":"IF door_open=TRUE THEN \"#ffeeaa\" ELSE \"#ac9393\" END" + }, + { + "id":"lift", + "attr":"y", + "value":"IF cur_floor=2 THEN \"3.207\" ELSIF cur_floor=1 THEN \"76.974\" ELSIF cur_floor=0 THEN \"150.474\" ELSE \"224.574\" END" + }, + { + "id":"door_right", + "attr":"y", + "value":"IF cur_floor=2 THEN \"3.207\" ELSIF cur_floor=1 THEN \"76.974\" ELSIF cur_floor=0 THEN \"150.474\" ELSE \"224.574\" END" + }, + { + "id":"door_left", + "attr":"y", + "value":"IF cur_floor=2 THEN \"3.207\" ELSIF cur_floor=1 THEN \"76.974\" ELSIF cur_floor=0 THEN \"150.474\" ELSE \"224.574\" END" + }, + { + "id":"button_U", + "attr":"fill", + "value":"IF -1:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"button_0", + "attr":"fill", + "value":"IF 0:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"button_1", + "attr":"fill", + "value":"IF 1:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"button_2", + "attr":"fill", + "value":"IF 2:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"inside_U", + "attr":"fill", + "value":"IF -1:inside_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"inside_0", + "attr":"fill", + "value":"IF 0:inside_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"inside_1", + "attr":"fill", + "value":"IF 1:inside_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"inside_2", + "attr":"fill", + "value":"IF 2:inside_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"reverse_up", + "attr":"visibility", + "value":"IF direction_up=TRUE THEN \"hidden\" ELSE \"visible\" END" + }, + { + "id":"reverse_down", + "attr":"visibility", + "value":"IF direction_up=FALSE THEN \"hidden\" ELSE \"visible\" END" + }, + { + "id":"open_door", + "attr":"visibility", + "value":"IF door_open=TRUE THEN \"hidden\" ELSE \"visible\" END" + }, + { + "id":"close_door", + "attr":"visibility", + "value":"IF door_open=FALSE THEN \"hidden\" ELSE \"visible\" END" + } + ], + "events":[ + { + "id":"button_U", + "event":"push_call_button", + "predicates":[ + "b=-1" + ] + }, + { + "id":"button_0", + "event":"push_call_button", + "predicates":[ + "b=0" + ] + }, + { + "id":"button_1", + "event":"push_call_button", + "predicates":[ + "b=1" + ] + }, + { + "id":"button_2", + "event":"push_call_button", + "predicates":[ + "b=2" + ] + }, + { + "id":"inside_U", + "event":"push_inside_button", + "predicates":[ + "b=-1" + ] + }, + { + "id":"inside_0", + "event":"push_inside_button", + "predicates":[ + "b=0" + ] + }, + { + "id":"inside_1", + "event":"push_inside_button", + "predicates":[ + "b=1" + ] + }, + { + "id":"inside_2", + "event":"push_inside_button", + "predicates":[ + "b=2" + ] + }, + { + "id":"close_door", + "event":"close_door" + }, + { + "id":"open_door", + "event":"open_door" + }, + { + "id":"up", + "event":"move_up" + }, + { + "id":"down", + "event":"move_down" + }, + { + "id":"reverse_up", + "event":"reverse_lift_up" + }, + { + "id":"reverse_down", + "event":"reverse_lift_down" + } + ] +} diff --git a/Lift/lift.svg b/Lift/lift.svg new file mode 100644 index 0000000000000000000000000000000000000000..3ad3f1d2dd0fdce6725f913cc2de1899dc79997b --- /dev/null +++ b/Lift/lift.svg @@ -0,0 +1,367 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<svg + xmlns:dc="http://purl.org/dc/elements/1.1/" + xmlns:cc="http://creativecommons.org/ns#" + xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" + xmlns:svg="http://www.w3.org/2000/svg" + xmlns="http://www.w3.org/2000/svg" + id="lift_visualsiation" + version="1.1" + viewBox="0 0 291.83881 295.06555" + height="295.06555" + width="291.83881"> + <defs + id="defs2" /> + <metadata + id="metadata5"> + <rdf:RDF> + <cc:Work + rdf:about=""> + <dc:format>image/svg+xml</dc:format> + <dc:type + rdf:resource="http://purl.org/dc/dcmitype/StillImage" /> + <dc:title></dc:title> + </cc:Work> + </rdf:RDF> + </metadata> + <g + transform="translate(-7.7786453,-0.86536193)" + id="layer1"> + <rect + y="0.86536193" + x="19.777943" + height="73.766388" + width="173.19066" + id="floor_2" + fill="#b3b3b3" + fill-opacity="1" + stroke-width="0.26458332" /> + <rect + y="74.631752" + x="19.777943" + height="73.766388" + width="173.19066" + id="floor_1" + fill="#cccccc" + fill-opacity="1" + stroke-width="0.26458332" /> + <rect + y="148.39813" + x="19.777943" + height="73.766388" + width="173.19066" + id="floor_0" + fill="#b3b3b3" + fill-opacity="1" + stroke-width="0.26458332" /> + <rect + y="222.16452" + x="19.777943" + height="73.766388" + width="173.19066" + id="floor_U" + fill="#cccccc" + fill-opacity="1" + stroke-width="0.26458332" /> + <text + id="text_2" + y="40.263763" + x="6.9466548" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + font-family="sans-serif" + letter-spacing="0px" + word-spacing="0px" + fill="#000000" + fill-opacity="1" + stroke="none" + stroke-width="0.26458332" + xml:space="preserve"><tspan + style="stroke-width:0.26458332" + y="40.263763" + x="6.9466548" + id="tspan861">2</tspan></text> + <text + id="text_1" + y="115.6209" + x="7.3037977" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + font-family="sans-serif" + letter-spacing="0px" + word-spacing="0px" + fill="#000000" + fill-opacity="1" + stroke="none" + stroke-width="0.26458332" + xml:space="preserve"><tspan + style="stroke-width:0.26458332" + y="115.6209" + x="7.3037977" + id="tspan4552">1</tspan></text> + <text + id="text_0" + y="186.3504" + x="8.0180836" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + font-family="sans-serif" + letter-spacing="0px" + word-spacing="0px" + fill="#000000" + fill-opacity="1" + stroke="none" + stroke-width="0.26458332" + xml:space="preserve"><tspan + style="stroke-width:0.26458332" + y="186.3504" + x="8.0180836" + id="tspan865">0</tspan></text> + <text + id="text_U" + y="259.58228" + x="8.0180836" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + font-family="sans-serif" + letter-spacing="0px" + word-spacing="0px" + fill="#000000" + fill-opacity="1" + stroke="none" + stroke-width="0.26458332" + xml:space="preserve"><tspan + style="stroke-width:0.26458332" + y="259.58228" + x="8.0180836" + id="tspan869">-1</tspan></text> + <rect + ry="0" + y="223.76816" + x="54.522984" + height="70.024597" + width="103.16602" + id="lift" + fill="#ffeeaa" + fill-opacity="1" + stroke-width="0.26458332" /> + <circle + r="6.1471992" + cy="258.78046" + cx="176.66516" + id="button_U" + fill="#ff8080" + fill-opacity="1" + stroke-width="0.26458332" /> + <circle + r="6.1471992" + cy="183.14319" + cx="175.86334" + id="button_0" + fill="#ff8080" + fill-opacity="1" + stroke-width="0.26458332" /> + <circle + r="6.1471992" + cy="109.91133" + cx="175.86334" + id="button_1" + fill="#ff8080" + fill-opacity="1" + stroke-width="0.26458332" /> + <circle + r="6.1471992" + cy="34.006786" + cx="176.39789" + id="button_2" + fill="#ff8080" + fill-opacity="1" + stroke-width="0.26458332" /> + <rect + fill="#ac9393" + fill-opacity="1" + stroke-width="0.26458332" + id="door_right" + width="34.210499" + height="70.024612" + x="54.522984" + y="223.76816" /> + <rect + fill="#ac9393" + fill-opacity="1" + stroke-width="0.26458332" + id="door_left" + width="34.210499" + height="70.024612" + x="123.47851" + y="223.76816" /> + <rect + y="73.781364" + x="209.26031" + height="148.02866" + width="90.35714" + id="rect4568" + fill="#999999" + fill-opacity="1" + stroke-width="1.26044464" /> + <path + d="m 235.46304,84.36361 3.47845,6.030475 3.63533,6.290954 -6.96176,-0.0028 -7.2658,0.0028 3.48332,-6.027661 z" + id="up" + fill="#ccff00" + fill-opacity="1" /> + <path + transform="scale(1,-0.99999992)" + d="m 275.52264,-96.68505 3.47845,6.030475 3.63533,6.290954 -6.96176,-0.0028 -7.2658,0.0028 3.48332,-6.027661 z" + id="down" + fill="#ccff00" + fill-opacity="1" /> + <path + d="m 235.46304,84.36361 3.47845,6.030475 3.63533,6.290954 -6.96176,-0.0028 -7.2658,0.0028 3.48332,-6.027661 z" + id="reverse_up" + fill="#ff8080" + fill-opacity="1" /> + <path + transform="scale(1,-0.99999992)" + d="m 275.52264,-96.68505 3.47845,6.030475 3.63533,6.290954 -6.96176,-0.0028 -7.2658,0.0028 3.48332,-6.027661 z" + id="reverse_down" + fill="#ff8080" + fill-opacity="1" /> + <text + id="inside_text_2" + y="116.0868" + x="230.22539" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + font-family="sans-serif" + letter-spacing="0px" + word-spacing="0px" + fill="#000000" + fill-opacity="1" + stroke="none" + stroke-width="0.26458332" + xml:space="preserve"><tspan + style="stroke-width:0.26458332" + y="116.0868" + x="230.22539" + id="tspan861-8">2</tspan></text> + <text + id="inside_text_1" + y="134.98444" + x="229.97792" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + font-family="sans-serif" + letter-spacing="0px" + word-spacing="0px" + fill="#000000" + fill-opacity="1" + stroke="none" + stroke-width="0.26458332" + xml:space="preserve"><tspan + style="stroke-width:0.26458332" + y="134.98444" + x="229.97792" + id="tspan4552-7">1</tspan></text> + <text + id="inside_text_0" + y="153.72188" + x="230.34941" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + font-family="sans-serif" + letter-spacing="0px" + word-spacing="0px" + fill="#000000" + fill-opacity="1" + stroke="none" + stroke-width="0.26458332" + xml:space="preserve"><tspan + style="stroke-width:0.26458332" + y="153.72188" + x="230.34941" + id="tspan865-0">0</tspan></text> + <text + id="inside_text_U" + y="172.77971" + x="226.33815" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + font-family="sans-serif" + letter-spacing="0px" + word-spacing="0px" + fill="#000000" + fill-opacity="1" + stroke="none" + stroke-width="0.26458332" + xml:space="preserve"><tspan + style="stroke-width:0.26458332" + y="172.77971" + x="226.33815" + id="tspan869-1">-1</tspan></text> + <circle + r="6.1471992" + cy="128.83723" + cx="276.07129" + id="inside_1" + fill="#ff8080" + fill-opacity="1" + stroke-width="0.26458332" /> + <circle + r="6.1471992" + cy="147.73488" + cx="276.07129" + id="inside_0" + fill="#ff8080" + fill-opacity="1" + stroke-width="0.26458332" /> + <circle + r="6.1471992" + cy="166.63251" + cx="276.07129" + id="inside_U" + fill="#ff8080" + fill-opacity="1" + stroke-width="0.26458332" /> + <circle + r="6.1471992" + cy="109.93961" + cx="276.07129" + id="inside_2" + fill="#ff8080" + fill-opacity="1" + stroke-width="0.26458332" /> + <circle + id="close_door" + fill="#ccff00" + fill-opacity="1" + stroke-width="0.26458332" + cx="255.13458" + cy="196.36461" + r="6.1471992"> + </circle> + <circle + id="open_door" + fill="#ccff00" + fill-opacity="1" + stroke-width="0.26458332" + cx="255.13458" + cy="196.36461" + r="6.1471992"> + </circle> +</svg> diff --git a/Lift/lift3.json b/Lift/lift3.json new file mode 100644 index 0000000000000000000000000000000000000000..255b4efa4dafa870c86981ba9e850e92043c3bf3 --- /dev/null +++ b/Lift/lift3.json @@ -0,0 +1,131 @@ +{ + "svg":"lift_groups.svg", + "items":[ + { + "id":"gFloor_2", + "attr":"visibility", + "value":"IF topf=2 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"gFloor_1", + "attr":"visibility", + "value":"IF topf:{1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"gFloor_0", + "attr":"visibility", + "value":"IF topf:{0,1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"gFloor_U", + "attr":"visibility", + "value":"IF groundf=-1 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"lift", + "attr":"fill", + "value":"IF door_open=TRUE THEN \"#ffeeaa\" ELSE \"#ac9393\" END" + }, + { + "id":"lift", + "attr":"y", + "value":"IF cur_floor=2 THEN \"grounf+3\" ELSIF cur_floor=1 THEN \"76.974\" ELSIF cur_floor=0 THEN \"150.474\" ELSE \"224.574\" END" + }, + { + "id":"door_right", + "attr":"y", + "value":"IF cur_floor=2 THEN \"3.207\" ELSIF cur_floor=1 THEN \"76.974\" ELSIF cur_floor=0 THEN \"150.474\" ELSE \"224.574\" END" + }, + { + "id":"door_left", + "attr":"y", + "value":"IF cur_floor=2 THEN \"3.207\" ELSIF cur_floor=1 THEN \"76.974\" ELSIF cur_floor=0 THEN \"150.474\" ELSE \"224.574\" END" + }, + { + "id":"button_U", + "attr":"fill", + "value":"IF -1:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"button_0", + "attr":"fill", + "value":"IF 0:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"button_1", + "attr":"fill", + "value":"IF 1:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"button_2", + "attr":"fill", + "value":"IF 2:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"reverse_up", + "attr":"visibility", + "value":"IF direction_up=TRUE THEN \"hidden\" ELSE \"visible\" END" + }, + { + "id":"reverse_down", + "attr":"visibility", + "value":"IF direction_up=FALSE THEN \"hidden\" ELSE \"visible\" END" + }, + { + "id":"open_door", + "attr":"visibility", + "value":"IF door_open=TRUE THEN \"hidden\" ELSE \"visible\" END" + } + ], + "events":[ + { + "id":"button_U", + "event":"push_call_button" + }, + { + "id":"button_0", + "event":"push_call_button", + "predicates":[ + "b=0" + ] + }, + { + "id":"button_1", + "event":"push_call_button", + "predicates":[ + "b=1" + ] + }, + { + "id":"button_2", + "event":"push_call_button", + "predicates":[ + "b=2" + ] + }, + { + "id":"close_door", + "event":"close_door" + }, + { + "id":"open_door", + "event":"open_door" + }, + { + "id":"up", + "event":"move_up" + }, + { + "id":"down", + "event":"move_down" + }, + { + "id":"reverse_up", + "event":"reverse_lift_up" + }, + { + "id":"reverse_down", + "event":"reverse_lift_down" + } + ] +} diff --git a/Lift/lift_groups.json b/Lift/lift_groups.json new file mode 100644 index 0000000000000000000000000000000000000000..dd7053f2ae82e072234cf1a94950c870e78a1330 --- /dev/null +++ b/Lift/lift_groups.json @@ -0,0 +1,182 @@ +{ + "svg":"lift_groups.svg", + "items":[ + { + "id":"gFloor_2", + "attr":"visibility", + "value":"IF topf=2 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"gFloor_1", + "attr":"visibility", + "value":"IF topf:{1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"gFloor_0", + "attr":"visibility", + "value":"IF topf:{0,1,2} THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"gFloor_U", + "attr":"visibility", + "value":"IF groundf=-1 THEN \"visible\" ELSE \"hidden\" END" + }, + { + "id":"lift", + "attr":"fill", + "value":"IF door_open=TRUE THEN \"#ffeeaa\" ELSE \"#ac9393\" END" + }, + { + "id":"lift", + "attr":"y", + "value":"IF cur_floor=2 THEN \"grounf+3\" ELSIF cur_floor=1 THEN \"76.974\" ELSIF cur_floor=0 THEN \"150.474\" ELSE \"224.574\" END" + }, + { + "id":"door_right", + "attr":"y", + "value":"IF cur_floor=2 THEN \"3.207\" ELSIF cur_floor=1 THEN \"76.974\" ELSIF cur_floor=0 THEN \"150.474\" ELSE \"224.574\" END" + }, + { + "id":"door_left", + "attr":"y", + "value":"IF cur_floor=2 THEN \"3.207\" ELSIF cur_floor=1 THEN \"76.974\" ELSIF cur_floor=0 THEN \"150.474\" ELSE \"224.574\" END" + }, + { + "id":"button_U", + "attr":"fill", + "value":"IF -1:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"button_0", + "attr":"fill", + "value":"IF 0:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"button_1", + "attr":"fill", + "value":"IF 1:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"button_2", + "attr":"fill", + "value":"IF 2:call_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"inside_U", + "attr":"fill", + "value":"IF -1:inside_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"inside_0", + "attr":"fill", + "value":"IF 0:inside_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"inside_1", + "attr":"fill", + "value":"IF 1:inside_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"inside_2", + "attr":"fill", + "value":"IF 2:inside_buttons THEN \"#FF0000\" ELSE \"#FF8080\" END" + }, + { + "id":"reverse_up", + "attr":"visibility", + "value":"IF direction_up=TRUE THEN \"hidden\" ELSE \"visible\" END" + }, + { + "id":"reverse_down", + "attr":"visibility", + "value":"IF direction_up=FALSE THEN \"hidden\" ELSE \"visible\" END" + }, + { + "id":"open_door", + "attr":"visibility", + "value":"IF door_open=TRUE THEN \"hidden\" ELSE \"visible\" END" + } + ], + "events":[ + { + "id":"button_U", + "event":"push_call_button", + "predicates":[ + "b=-1" + ] + }, + { + "id":"button_0", + "event":"push_call_button", + "predicates":[ + "b=0" + ] + }, + { + "id":"button_1", + "event":"push_call_button", + "predicates":[ + "b=1" + ] + }, + { + "id":"button_2", + "event":"push_call_button", + "predicates":[ + "b=2" + ] + }, + { + "id":"inside_U", + "event":"push_inside_button", + "predicates":[ + "b=-1" + ] + }, + { + "id":"inside_0", + "event":"push_inside_button", + "predicates":[ + "b=0" + ] + }, + { + "id":"inside_1", + "event":"push_inside_button", + "predicates":[ + "b=1" + ] + }, + { + "id":"inside_2", + "event":"push_inside_button", + "predicates":[ + "b=2" + ] + }, + { + "id":"close_door", + "event":"close_door" + }, + { + "id":"open_door", + "event":"open_door" + }, + { + "id":"up", + "event":"move_up" + }, + { + "id":"down", + "event":"move_down" + }, + { + "id":"reverse_up", + "event":"reverse_lift_up" + }, + { + "id":"reverse_down", + "event":"reverse_lift_down" + } + ] +} diff --git a/Lift/lift_groups.svg b/Lift/lift_groups.svg new file mode 100644 index 0000000000000000000000000000000000000000..e1ff3b18f9a2a39c8852cfd8b853290dcbbd7ae0 --- /dev/null +++ b/Lift/lift_groups.svg @@ -0,0 +1,377 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<svg + xmlns:dc="http://purl.org/dc/elements/1.1/" + xmlns:cc="http://creativecommons.org/ns#" + xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" + xmlns:svg="http://www.w3.org/2000/svg" + xmlns="http://www.w3.org/2000/svg" + width="291.83881" + height="295.06555" + viewBox="0 0 291.83881 295.06555" + version="1.1" + id="lift_visualsiation"> + <defs + id="defs2" /> + <metadata + id="metadata5"> + <rdf:RDF> + <cc:Work + rdf:about=""> + <dc:format>image/svg+xml</dc:format> + <dc:type + rdf:resource="http://purl.org/dc/dcmitype/StillImage" /> + <dc:title></dc:title> + </cc:Work> + </rdf:RDF> + </metadata> + <g + id="layer1" + transform="translate(-7.7786453,-0.86536193)"> + <rect + fill="#999999" + fill-opacity="1" + stroke-width="1.26044464" + id="rect4568" + width="90.35714" + height="148.02866" + x="209.26031" + y="73.781364" /> + <path + fill="#ccff00" + fill-opacity="1" + id="up" + d="m 235.46304,84.36361 3.47845,6.030475 3.63533,6.290954 -6.96176,-0.0028 -7.2658,0.0028 3.48332,-6.027661 z" /> + <path + fill="#ccff00" + fill-opacity="1" + id="down" + d="m 275.52264,-96.68505 3.47845,6.030475 3.63533,6.290954 -6.96176,-0.0028 -7.2658,0.0028 3.48332,-6.027661 z" + transform="scale(1,-0.99999992)" /> + <path + fill="#ff8080" + fill-opacity="1" + id="reverse_up" + d="m 235.46304,84.36361 3.47845,6.030475 3.63533,6.290954 -6.96176,-0.0028 -7.2658,0.0028 3.48332,-6.027661 z" /> + <path + fill="#ff8080" + fill-opacity="1" + id="reverse_down" + d="m 275.52264,-96.68505 3.47845,6.030475 3.63533,6.290954 -6.96176,-0.0028 -7.2658,0.0028 3.48332,-6.027661 z" + transform="scale(1,-0.99999992)" /> + <g + id="gFloor_1"> + <rect + y="74.631752" + x="19.777943" + height="73.766388" + width="173.19066" + id="floor_1" + stroke-width="0.26458332" + fill-opacity="1" + fill="#cccccc" /> + <text + id="text_1" + y="115.6209" + x="7.3037977" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + letter-spacing="0px" + word-spacing="0px" + xml:space="preserve" + style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"><tspan + style="stroke-width:0.26458332" + y="115.6209" + x="7.3037977" + id="tspan4552">1</tspan></text> + <circle + r="6.1471992" + cy="109.91133" + cx="175.86334" + id="button_1" + stroke-width="0.26458332" + fill-opacity="1" + fill="#ff8080" /> + <text + id="inside_text_1" + y="134.98444" + x="229.97792" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + letter-spacing="0px" + word-spacing="0px" + xml:space="preserve" + font-family="sans-serif" + stroke-width="0.26458332" + stroke="none" + fill-opacity="1" + fill="#000000"><tspan + style="stroke-width:0.26458332" + y="134.98444" + x="229.97792" + id="tspan4552-7">1</tspan></text> + <circle + r="6.1471992" + cy="128.83723" + cx="276.07129" + id="inside_1" + stroke-width="0.26458332" + fill-opacity="1" + fill="#ff8080" /> + </g> + <g + id="gFloor_0"> + <rect + y="148.39813" + x="19.777943" + height="73.766388" + width="173.19066" + id="floor_0" + stroke-width="0.26458332" + fill-opacity="1" + fill="#b3b3b3" /> + <text + id="text_0" + y="186.3504" + x="8.0180836" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + letter-spacing="0px" + word-spacing="0px" + xml:space="preserve" + font-family="sans-serif" + stroke-width="0.26458332" + stroke="none" + fill-opacity="1" + fill="#000000"><tspan + style="stroke-width:0.26458332" + y="186.3504" + x="8.0180836" + id="tspan865">0</tspan></text> + <circle + r="6.1471992" + cy="183.14319" + cx="175.86334" + id="button_0" + stroke-width="0.26458332" + fill-opacity="1" + fill="#ff8080" /> + <text + id="inside_text_0" + y="153.72188" + x="230.34941" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + letter-spacing="0px" + word-spacing="0px" + xml:space="preserve" + font-family="sans-serif" + stroke-width="0.26458332" + stroke="none" + fill-opacity="1" + fill="#000000"><tspan + style="stroke-width:0.26458332" + y="153.72188" + x="230.34941" + id="tspan865-0">0</tspan></text> + <circle + r="6.1471992" + cy="147.73488" + cx="276.07129" + id="inside_0" + stroke-width="0.26458332" + fill-opacity="1" + fill="#ff8080" /> + </g> + <g + id="gFloor_U"> + <rect + y="222.16452" + x="19.777943" + height="73.766388" + width="173.19066" + id="floor_U" + fill="#cccccc" + fill-opacity="1" + stroke-width="0.26458332" /> + <text + id="text_U" + y="259.58228" + x="8.0180836" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + font-family="sans-serif" + letter-spacing="0px" + word-spacing="0px" + fill="#000000" + fill-opacity="1" + stroke="none" + stroke-width="0.26458332" + xml:space="preserve"><tspan + style="stroke-width:0.26458332" + y="259.58228" + x="8.0180836" + id="tspan869">-1</tspan></text> + <circle + r="6.1471992" + cy="258.78046" + cx="176.66516" + id="button_U" + fill="#ff8080" + fill-opacity="1" + stroke-width="0.26458332" /> + <text + id="inside_text_U" + y="172.77971" + x="226.33815" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + font-family="sans-serif" + letter-spacing="0px" + word-spacing="0px" + fill="#000000" + fill-opacity="1" + stroke="none" + stroke-width="0.26458332" + xml:space="preserve"><tspan + style="stroke-width:0.26458332" + y="172.77971" + x="226.33815" + id="tspan869-1">-1</tspan></text> + <circle + r="6.1471992" + cy="166.63251" + cx="276.07129" + id="inside_U" + fill="#ff8080" + fill-opacity="1" + stroke-width="0.26458332" /> + </g> + <g + id="gFloor_2"> + <rect + y="0.86536193" + x="19.777943" + height="73.766388" + width="173.19066" + id="floor_2" + stroke-width="0.26458332" + fill-opacity="1" + fill="#b3b3b3" /> + <text + id="text_2" + y="40.263763" + x="6.9466548" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + letter-spacing="0px" + word-spacing="0px" + xml:space="preserve" + font-family="sans-serif" + stroke-width="0.26458332" + stroke="none" + fill-opacity="1" + fill="#000000"><tspan + style="stroke-width:0.26458332" + y="40.263763" + x="6.9466548" + id="tspan861">2</tspan></text> + <circle + r="6.1471992" + cy="34.006786" + cx="176.39789" + id="button_2" + stroke-width="0.26458332" + fill-opacity="1" + fill="#ff8080" /> + <text + id="inside_text_2" + y="116.0868" + x="230.22539" + font-style="normal" + font-weight="normal" + font-size="10.58333302px" + line-height="1.25" + letter-spacing="0px" + word-spacing="0px" + xml:space="preserve" + font-family="sans-serif" + stroke-width="0.26458332" + stroke="none" + fill-opacity="1" + fill="#000000"><tspan + style="stroke-width:0.26458332" + y="116.0868" + x="230.22539" + id="tspan861-8">2</tspan></text> + <circle + r="6.1471992" + cy="109.93961" + cx="276.07129" + id="inside_2" + stroke-width="0.26458332" + fill-opacity="1" + fill="#ff8080" /> + </g> + <circle + fill="#ccff00" + fill-opacity="1" + stroke-width="0.26458332" + r="6.1471992" + cy="196.36461" + cx="255.13458" + id="close_door" /> + <circle + fill="#ccff00" + fill-opacity="1" + stroke-width="0.26458332" + r="6.1471992" + cy="196.36461" + cx="255.13458" + id="open_door" /> + </g> + <g + style="display:inline"> + <rect + id="lift" + ry="0" + y="223.76816" + x="54.522984" + height="70.024597" + width="103.16602" + id="lift" + fill="#ffeeaa" + fill-opacity="1" + stroke-width="0.26458332" + transform="translate(-7.7786453,-0.86536193)" /> + <rect + y="223.76816" + x="54.522984" + height="70.024612" + width="34.210499" + id="door_right" + style="fill:#ac9393;fill-opacity:1;stroke-width:0.26458332" + transform="translate(-7.7786453,-0.86536193)" /> + <rect + y="223.76816" + x="123.47851" + height="70.024612" + width="34.210499" + id="door_left" + style="fill:#ac9393;fill-opacity:1;stroke-width:0.26458332" + transform="translate(-7.7786453,-0.86536193)" /> + </g> +</svg>