Skip to content
Snippets Groups Projects
Commit 04de62bd authored by Fabian Vu's avatar Fabian Vu
Browse files

Merge branch 'master' of... 

Merge branch 'master' of https://gitlab.cs.uni-duesseldorf.de/general/stups/visb-visualisation-examples
parents 29ff29da 4a7c644b
No related branches found
No related tags found
No related merge requests found
Expand all Show whitespace changes
Inline Side-by-side
Button/button2.json
+ 3
− 1
View file @ 04de62bd
{
"svg": "button.svg",
"model": "button2.mch",
"model-name": "button2",
"items": [
{
......
Button/button2.mch
+ 2
− 2
View file @ 04de62bd
LandingGear/LandingGear.json
+ 1
− 0
View file @ 04de62bd
{
"svg":"architecture.svg",
"model":"R6GearsDoorsHandleValvesControllerSwitch",
"items":[
{
"repeat": ["1", "2", "3"],
......
TrafficLight/traffic_light.json
+ 1
− 0
View file @ 04de62bd
{
"svg":"traffic_light.svg",
"model-name":"TrafficLight",
"items":[
{
"id":"cars_red",
......
Train_B_Book/train.json
+ 4
− 4
View file @ 04de62bd
......@@ -13,7 +13,7 @@
"attr": "stroke",
"value": "IF %0 : OCC THEN \"#FF2222\" ELSE IF %0 : resbl THEN \"#2222FF\" ELSE \"#000000\" END END",
"repeat": [
["A"], ["B"], ["C"], ["D"], ["E"], ["F"], ["G"], ["H"], ["I"], ["J"], ["K"], ["L"], ["M"], ["N"]
["A"], ["B"], ["C"], ["D"], ["E"], ["F"], ["G"], ["H"], ["I"], ["J"], ["L"], ["M"], ["N"]
]
},
{
......@@ -109,7 +109,7 @@
"for": {"from":1, "to":5},
"id": "s%0",
"event": "route_formation",
"predicates": ["r : (%s.s:S|fst~[SIG~[{s}]])(S%0)"]
"predicates": ["r : %s.(s:S|fst~[SIG~[{s}]])(S%0)"]
},
{
"id": "%0_start",
......@@ -124,7 +124,7 @@
"event": "FRONT_MOVE_2",
"predicates": ["b=%0"],
"repeat": [
["A"], ["B"],["C"], ["D"], ["E"], ["F"], ["G"], ["H"], ["I"], ["J"], ["K"], ["L"], ["M"], ["N"]
["A"], ["B"],["C"], ["D"], ["E"], ["F"], ["G"], ["H"], ["I"], ["J"], ["K"], ["N"]
]
},
{
......@@ -132,7 +132,7 @@
"event": "FRONT_MOVE_2",
"predicates": ["b=%0"],
"repeat": [
["A"], ["B"],["C"], ["D"], ["E"], ["F"], ["G"], ["H"], ["I"], ["J"], ["K"], ["L"], ["M"], ["N"]
["A"], ["B"], ["D"], ["E"], ["F"], ["H"], ["I"], ["J"], ["K"], ["L"], ["M"]
]
},
{
......
Train_B_Book/train4.json 0 → 100644
+ 17
− 0
View file @ 04de62bd
{
"svg": "train.svg",
"include": "train1.json",
"model-name": "train_4_POR",
"items": [
{
"for": {"from":1, "to":5},
"id": "s%0_red",
"attr": "fill",
"value": "IF S%0 : GRN THEN \"#FFD5D5\" ELSE \"#FF2222\" END",
"override": "true"
}
],
"events": [
]
}
Train_B_Book/train_4_POR_mch.html 0 → 100644
+ 6108
− 0
View file @ 04de62bd
This diff is collapsed.
Train_B_Book/train_4_POR_mch.prob2trace 0 → 100644
+ 882
− 0
View file @ 04de62bd
{
"description": "File created by ProB Tcl/Tk",
"transitionList": [
{
"name": "$setup_constants",
"destState": {
"rtbl": "{(A|->R1),(A|->R2),(A|->R3),(A|->R6),(A|->R7),(A|->R8),(B|->R1),(B|->R2),(B|->R3),(B|->R6),(B|->R7),(B|->R8),(C|->R1),(C|->R6),(D|->R2),(D|->R3),(D|->R7),(D|->R8),(E|->R2),(E|->R7),(F|->R2),(F|->R4),(F|->R7),(F|->R9),(G|->R2),(G|->R4),(G|->R7),(G|->R9),(H|->R4),(H|->R5),(H|->R9),(H|->R10),(I|->R4),(I|->R5),(I|->R9),(I|->R10),(J|->R3),(J|->R5),(J|->R8),(J|->R10),(K|->R3),(K|->R4),(K|->R8),(K|->R9),(L|->R1),(L|->R2),(L|->R3),(L|->R6),(L|->R7),(L|->R8),(M|->R4),(M|->R5),(M|->R9),(M|->R10),(N|->R3),(N|->R5),(N|->R8),(N|->R10)}",
"lst": "{(R1|->C),(R2|->G),(R3|->N),(R4|->G),(R5|->N),(R6|->L),(R7|->L),(R8|->L),(R9|->M),(R10|->M)}",
"nxt": "{(R1|->{(A|->B),(B|->C),(L|->A)}),(R2|->{(A|->B),(B|->D),(D|->E),(E|->F),(F|->G),(L|->A)}),(R3|->{(A|->B),(B|->D),(D|->K),(J|->N),(K|->J),(L|->A)}),(R4|->{(F|->G),(H|->I),(I|->K),(K|->F),(M|->H)}),(R5|->{(H|->I),(I|->J),(J|->N),(M|->H)}),(R6|->{(A|->L),(B|->A),(C|->B)}),(R7|->{(A|->L),(B|->A),(D|->B),(E|->D),(F|->E),(G|->F)}),(R8|->{(A|->L),(B|->A),(D|->B),(J|->K),(K|->D),(N|->J)}),(R9|->{(F|->K),(G|->F),(H|->M),(I|->H),(K|->I)}),(R10|->{(H|->M),(I|->H),(J|->I),(N|->J)})}",
"fst": "{(R1|->L),(R2|->L),(R3|->L),(R4|->M),(R5|->M),(R6|->C),(R7|->G),(R8|->N),(R9|->G),(R10|->N)}",
"SIG": "{(C|->S4),(G|->S5),(L|->S1),(M|->S2),(N|->S3)}",
"rht": "{(B|->A),(D|->A),(F|->A),(I|->A),(J|->A)}",
"lft": "{(B|->B),(D|->B),(F|->B),(I|->B),(J|->B)}",
"blpt": "{B,D,F,I,J}"
},
"destStateNotChanged": [
]
},
{
"name": "$initialise_machine",
"destState": {
"GRN": "{}",
"LBT": "{}",
"OCC": "{}",
"TRK": "{}",
"frm": "{}",
"rdy": "{}",
"resbl": "{}",
"resrt": "{}",
"rsrtbl": "{}"
},
"destStateNotChanged": [
]
},
{
"name": "route_reservation",
"params": {
"r": "R9"
},
"destState": {
"resbl": "{F,G,H,I,K,M}",
"resrt": "{R9}",
"rsrtbl": "{(F|->R9),(G|->R9),(H|->R9),(I|->R9),(K|->R9),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"frm",
"rdy"
]
},
{
"name": "point_positionning",
"params": {
"r": "R9"
},
"destState": {
"TRK": "{(F|->K),(G|->F),(H|->M),(I|->H),(K|->I)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "route_reservation",
"params": {
"r": "R1"
},
"destState": {
"resbl": "{A,B,C,F,G,H,I,K,L,M}",
"resrt": "{R1,R9}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(F|->R9),(G|->R9),(H|->R9),(I|->R9),(K|->R9),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"frm",
"rdy"
]
},
{
"name": "route_formation",
"params": {
"r": "R9"
},
"destState": {
"GRN": "{S5}",
"frm": "{R9}",
"rdy": "{R9}"
},
"destStateNotChanged": [
"LBT",
"OCC",
"TRK",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_1",
"params": {
"b": "G"
},
"destState": {
"GRN": "{}",
"LBT": "{G}",
"OCC": "{G}",
"rdy": "{}"
},
"destStateNotChanged": [
"TRK",
"frm",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "G"
},
"destState": {
"OCC": "{F,G}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "G"
},
"destState": {
"LBT": "{F}",
"OCC": "{F}",
"resbl": "{A,B,C,F,H,I,K,L,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(F|->R9),(H|->R9),(I|->R9),(K|->R9),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "F"
},
"destState": {
"OCC": "{F,K}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "F"
},
"destState": {
"LBT": "{K}",
"OCC": "{K}",
"resbl": "{A,B,C,H,I,K,L,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(H|->R9),(I|->R9),(K|->R9),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "point_positionning",
"params": {
"r": "R1"
},
"destState": {
"TRK": "{(A|->B),(B|->C),(F|->K),(G|->F),(H|->M),(I|->H),(K|->I),(L|->A)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "K"
},
"destState": {
"OCC": "{I,K}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "K"
},
"destState": {
"LBT": "{I}",
"OCC": "{I}",
"resbl": "{A,B,C,H,I,L,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(H|->R9),(I|->R9),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "I"
},
"destState": {
"OCC": "{H,I}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "I"
},
"destState": {
"LBT": "{H}",
"OCC": "{H}",
"resbl": "{A,B,C,H,L,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(H|->R9),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "H"
},
"destState": {
"OCC": "{H,M}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "H"
},
"destState": {
"LBT": "{M}",
"OCC": "{M}",
"resbl": "{A,B,C,L,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(L|->R1),(M|->R9)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "BACK_MOVE_1",
"params": {
"b": "M"
},
"destState": {
"LBT": "{}",
"OCC": "{}",
"resbl": "{A,B,C,L}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(L|->R1)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "route_freeing",
"params": {
"r": "R9"
},
"destState": {
"frm": "{}",
"resrt": "{R1}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"rdy",
"resbl",
"rsrtbl"
]
},
{
"name": "route_reservation",
"params": {
"r": "R4"
},
"destState": {
"resbl": "{A,B,C,F,G,H,I,K,L,M}",
"resrt": "{R1,R4}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4),(L|->R1),(M|->R4)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"frm",
"rdy"
]
},
{
"name": "route_formation",
"params": {
"r": "R1"
},
"destState": {
"GRN": "{S1}",
"frm": "{R1}",
"rdy": "{R1}"
},
"destStateNotChanged": [
"LBT",
"OCC",
"TRK",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_1",
"params": {
"b": "L"
},
"destState": {
"GRN": "{}",
"LBT": "{L}",
"OCC": "{L}",
"rdy": "{}"
},
"destStateNotChanged": [
"TRK",
"frm",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "L"
},
"destState": {
"OCC": "{A,L}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "point_positionning",
"params": {
"r": "R4"
},
"destState": {
"TRK": "{(A|->B),(B|->C),(F|->G),(H|->I),(I|->K),(K|->F),(L|->A),(M|->H)}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "A"
},
"destState": {
"OCC": "{A,B,L}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "B"
},
"destState": {
"OCC": "{A,B,C,L}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "L"
},
"destState": {
"LBT": "{A}",
"OCC": "{A,B,C}",
"resbl": "{A,B,C,F,G,H,I,K,M}",
"rsrtbl": "{(A|->R1),(B|->R1),(C|->R1),(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4),(M|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "A"
},
"destState": {
"LBT": "{B}",
"OCC": "{B,C}",
"resbl": "{B,C,F,G,H,I,K,M}",
"rsrtbl": "{(B|->R1),(C|->R1),(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4),(M|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "route_formation",
"params": {
"r": "R4"
},
"destState": {
"GRN": "{S2}",
"frm": "{R1,R4}",
"rdy": "{R4}"
},
"destStateNotChanged": [
"LBT",
"OCC",
"TRK",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_1",
"params": {
"b": "M"
},
"destState": {
"GRN": "{}",
"LBT": "{B,M}",
"OCC": "{B,C,M}",
"rdy": "{}"
},
"destStateNotChanged": [
"TRK",
"frm",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "M"
},
"destState": {
"OCC": "{B,C,H,M}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "B"
},
"destState": {
"LBT": "{C,M}",
"OCC": "{C,H,M}",
"resbl": "{C,F,G,H,I,K,M}",
"rsrtbl": "{(C|->R1),(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4),(M|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "BACK_MOVE_1",
"params": {
"b": "C"
},
"destState": {
"LBT": "{M}",
"OCC": "{H,M}",
"resbl": "{F,G,H,I,K,M}",
"rsrtbl": "{(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4),(M|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "route_freeing",
"params": {
"r": "R1"
},
"destState": {
"frm": "{R4}",
"resrt": "{R4}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"rdy",
"resbl",
"rsrtbl"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "H"
},
"destState": {
"OCC": "{H,I,M}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "M"
},
"destState": {
"LBT": "{H}",
"OCC": "{H,I}",
"resbl": "{F,G,H,I,K}",
"rsrtbl": "{(F|->R4),(G|->R4),(H|->R4),(I|->R4),(K|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "H"
},
"destState": {
"LBT": "{I}",
"OCC": "{I}",
"resbl": "{F,G,I,K}",
"rsrtbl": "{(F|->R4),(G|->R4),(I|->R4),(K|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "I"
},
"destState": {
"OCC": "{I,K}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "I"
},
"destState": {
"LBT": "{K}",
"OCC": "{K}",
"resbl": "{F,G,K}",
"rsrtbl": "{(F|->R4),(G|->R4),(K|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "K"
},
"destState": {
"OCC": "{F,K}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "K"
},
"destState": {
"LBT": "{F}",
"OCC": "{F}",
"resbl": "{F,G}",
"rsrtbl": "{(F|->R4),(G|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "FRONT_MOVE_2",
"params": {
"b": "F"
},
"destState": {
"OCC": "{F,G}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"TRK",
"frm",
"rdy",
"resbl",
"resrt",
"rsrtbl"
]
},
{
"name": "BACK_MOVE_2",
"params": {
"b": "F"
},
"destState": {
"LBT": "{G}",
"OCC": "{G}",
"resbl": "{G}",
"rsrtbl": "{(G|->R4)}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "BACK_MOVE_1",
"params": {
"b": "G"
},
"destState": {
"LBT": "{}",
"OCC": "{}",
"resbl": "{}",
"rsrtbl": "{}"
},
"destStateNotChanged": [
"GRN",
"TRK",
"frm",
"rdy",
"resrt"
]
},
{
"name": "route_freeing",
"params": {
"r": "R4"
},
"destState": {
"frm": "{}",
"resrt": "{}"
},
"destStateNotChanged": [
"GRN",
"LBT",
"OCC",
"TRK",
"rdy",
"resbl",
"rsrtbl"
]
}
],
"metadata": {
"fileType": "Trace",
"formatVersion": 1,
"savedAt": "2022-05-25T17:18:52Z",
"creator": "tcltk (leuschel)",
"proBCliVersion": "1.12.0-nightly",
"proBCliRevision": "94b13de9d6fba932404838299859bea55586e8aa",
"modelName": "train_4_POR",
"modelFile": "/Users/leuschel/git_root/JAVAPROB/visb-visualisation-examples/Train_B_Book/train_4_POR_mch.eventb"
}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment