Commit b493fddf authored by Michael Leuschel's avatar Michael Leuschel
Browse files

also visualize train position in example

parent be0fdb7a
...@@ -4,7 +4,7 @@ MACHINE TrainTrack ...@@ -4,7 +4,7 @@ MACHINE TrainTrack
SETS SETS
TTDS = {ttd1,ttd2,ttd3} TTDS = {ttd1,ttd2,ttd3}
CONSTANTS CONSTANTS
TrackElementNumber, TRACK, TTD_TrackElements TrackElementNumber, TRACK, TTD_TrackElements, train_length
PROPERTIES PROPERTIES
TrackElementNumber : NATURAL1 TrackElementNumber : NATURAL1
& TRACK = 0..TrackElementNumber & TRACK = 0..TrackElementNumber
...@@ -13,17 +13,23 @@ PROPERTIES ...@@ -13,17 +13,23 @@ PROPERTIES
& TrackElementNumber = 30 & TrackElementNumber = 30
& TTD_TrackElements = {ttd1 |-> 0..10 , ttd2 |-> 11..25 , ttd3 |-> 26..30} & TTD_TrackElements = {ttd1 |-> 0..10 , ttd2 |-> 11..25 , ttd3 |-> 26..30}
& train_length = 2
VARIABLES VARIABLES
occ occ,
train_rear_end
INVARIANT INVARIANT
occ <: TTDS occ <: TTDS &
INITIALISATION occ := {} train_rear_end : TRACK
INITIALISATION occ := {} || train_rear_end := 0
OPERATIONS OPERATIONS
TTD_Occupied(ttd) = PRE ttd:TTDS \ occ THEN TTD_Occupied(ttd) = PRE ttd:TTDS \ occ THEN
occ := occ \/ {ttd} occ := occ \/ {ttd}
END; END;
TTD_Free(ttd) = PRE ttd:occ THEN TTD_Free(ttd) = PRE ttd:occ THEN
occ := occ \ {ttd} occ := occ \ {ttd}
END;
TrainMoveForward = PRE train_rear_end+1:TRACK THEN
train_rear_end := train_rear_end + 1
END END
DEFINITIONS DEFINITIONS
"LibrarySVG.def"; // enable to use the external functions in the VisB json file "LibrarySVG.def"; // enable to use the external functions in the VisB json file
......
...@@ -2,6 +2,13 @@ ...@@ -2,6 +2,13 @@
"svg":"Track.svg", "svg":"Track.svg",
"items":[ "items":[
{
"id":"train_polygon",
"attr":"points",
"value":"svg_train(train_rear_end, train_length ,100.0/real(TrackElementNumber+1),1.0,3.0)",
"comment":"show train position using a slanted polygon"
},
{ {
"id":"track_polyline", "id":"track_polyline",
"attr":"points", "attr":"points",
...@@ -18,13 +25,13 @@ ...@@ -18,13 +25,13 @@
"id":"occupied_ttd_polygon", "id":"occupied_ttd_polygon",
"attr":"points", "attr":"points",
"value":"svg_set_polygon(OCC_TE,100.0/real(TrackElementNumber+1),100.0,2.0)", "value":"svg_set_polygon(OCC_TE,100.0/real(TrackElementNumber+1),100.0,2.0)",
"comment":"show ticks for TTD Limits" "comment":"show occupied TTD zones"
}, },
{ {
"id":"cleared_ttd_polygon", "id":"cleared_ttd_polygon",
"attr":"points", "attr":"points",
"value":"svg_set_polygon(FREE_TE,100.0/real(TrackElementNumber+1),100.0,2.0)", "value":"svg_set_polygon(FREE_TE,100.0/real(TrackElementNumber+1),100.0,2.0)",
"comment":"show ticks for TTD Limits" "comment":"show free TTD zones"
} }
], ],
"events":[ "events":[
...@@ -41,6 +48,13 @@ ...@@ -41,6 +48,13 @@
"optional" : true, "optional" : true,
"hovers": [{ "attr":"stroke", "enter":"black", "leave":"none"}, "hovers": [{ "attr":"stroke", "enter":"black", "leave":"none"},
{ "attr":"opacity", "enter":"0.5", "leave":"1.0"}] { "attr":"opacity", "enter":"0.5", "leave":"1.0"}]
},
{
"id":"train_polygon",
"event":"TrainMoveForward",
"optional" : true,
"hovers": [{ "attr":"fill", "enter":"red", "leave":"lightgray"},
{ "attr":"stroke-width", "enter":"0.5", "leave":"0.3"}]
} }
] ]
} }
\ No newline at end of file
...@@ -7,6 +7,12 @@ ...@@ -7,6 +7,12 @@
version="1.1" version="1.1"
id="svg5154"> id="svg5154">
<polygon id = "train_polygon"
points="0,0 100,0"
style="stroke-width: 0.3"
stroke="black" fill="lightgray"
transform="translate(10,16.8)" />
<polygon id = "track_polyline" <polygon id = "track_polyline"
points="0,0 1,0, 1,1 1,0 50,0 50,1 50,0 100,0" points="0,0 1,0, 1,1 1,0 50,0 50,1 50,0 100,0"
style="stroke-width: 0.3" style="stroke-width: 0.3"
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment