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

add old lift

parent 37221d3d
Branches
No related tags found
No related merge requests found
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
{
"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"
}
]
}
<?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>
{
"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"
}
]
}
{
"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"
}
]
}
<?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>
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment