@startuml model_11.puml
skinparam state {
  BackgroundColor<<normal>> White
  BackgroundColor<<barrier>> Red
  BackgroundColor<<oil_spill>> Yellow
  BackgroundColor<<charging>> Green
}

state "l1 <<blocked>>" as loc1:Inv: x1==0 \n x2==0, c>=0.1\nFlow: x1'==0 \n x2'==0, c'==-1
state "l2 <<normal>>" as loc2:Inv: 1<=x1<=2\n 0<=x2<=1, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-1
state "l3 <<charging>>" as loc3:Inv: 2<=x1<=3\n 0<=x2<=1, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==0
state "l4 <<normal>>" as loc4:Inv: 3<=x1<=4\n 0<=x2<=1, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-1
state "l5 <<blocked>>" as loc5:Inv: x1==0 \n x2==0, c>=0.1\nFlow: x1'==0 \n x2'==0, c'==-1
state "l6 <<normal>>" as loc6:Inv: 1<=x1<=2\n 1<=x2<=2, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-1
state "l7 <<normal>>" as loc7:Inv: 2<=x1<=3\n 1<=x2<=2, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-1
state "l8 <<oil_spill>" as loc8:Inv: 3<=x1<=4\n 1<=x2<=2, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-2
state "l9 <<oil_spill>" as loc9:Inv: 0<=x1<=1\n 2<=x2<=3, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-2
state "l10 <<blocked>>" as loc10:Inv: x1==0 \n x2==0, c>=0.1\nFlow: x1'==0 \n x2'==0, c'==-1
state "l11 <<normal>>" as loc11:Inv: 2<=x1<=3\n 2<=x2<=3, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-1
state "l12 <<normal>>" as loc12:Inv: 3<=x1<=4\n 2<=x2<=3, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-1
state "l13 <<normal>>" as loc13:Inv: 0<=x1<=1\n 3<=x2<=4, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-1
state "l14 <<normal>>" as loc14:Inv: 1<=x1<=2\n 3<=x2<=4, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-1
state "l15 <<normal>>" as loc15:Inv: 2<=x1<=3\n 3<=x2<=4, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-1
state "l16 <<normal>>" as loc16:Inv: 3<=x1<=4\n 3<=x2<=4, c>=0.1\nFlow: -1<=x1'<=1 \n -1<=x2'<=1, c'==-1

loc1-right[#white]->loc2
loc1-up[#white]->loc5
loc2 -right-> loc3: e1\n x1 ==2,0<=x2<1
loc3 -down-> loc2: e2\n1<=x1<2, x2==1\n c := 10
loc2 -up-> loc6: e3\n1<=x1<2, x2==1
loc6 -down-> loc2: e4\n1<=x1<2, x2==1
loc3 -right-> loc4: e5\n x1 ==3,0<=x2<1\n c := 10
loc4 -left-> loc3: e6\n x1 ==3,0<=x2<1
loc3 -up-> loc7: e7\n2<=x1<3, x2==1\n c := 10
loc7 -down-> loc3: e8\n2<=x1<3, x2==1
loc4 -up-> loc8: e9\n3<=x1<4, x2==1
loc8 -down-> loc4: e10\n3<=x1<4, x2==1
loc5-right[#white]->loc6
loc5-up[#white]->loc9
loc6 -right-> loc7: e11\n x1 ==2,1<=x2<2
loc7 -left-> loc6: e12\n x1 ==2,1<=x2<2
loc6-up[#white]->loc10
loc7 -right-> loc8: e13\n x1 ==3,1<=x2<2
loc8 -left-> loc7: e14\n x1 ==3,1<=x2<2
loc7 -up-> loc11: e15\n2<=x1<3, x2==2
loc11 -down-> loc7: e16\n2<=x1<3, x2==2
loc8 -up-> loc12: e17\n3<=x1<4, x2==2
loc12 -down-> loc8: e18\n3<=x1<4, x2==2
loc9-right[#white]->loc10
loc9 -up-> loc13: e19\n0<=x1<1, x2==3
loc13 -down-> loc9: e20\n0<=x1<1, x2==3
loc10-right[#white]->loc11
loc10-up[#white]->loc14
loc11 -right-> loc12: e21\n x1 ==3,2<=x2<3
loc12 -left-> loc11: e22\n x1 ==3,2<=x2<3
loc11 -up-> loc15: e23\n2<=x1<3, x2==3
loc15 -down-> loc11: e24\n2<=x1<3, x2==3
loc12 -up-> loc16: e25\n3<=x1<4, x2==3
loc16 -down-> loc12: e26\n3<=x1<4, x2==3
loc13 -right-> loc14: e27\n x1 ==1,3<=x2<4
loc14 -left-> loc13: e28\n x1 ==1,3<=x2<4
loc14 -right-> loc15: e29\n x1 ==2,3<=x2<4
loc15 -left-> loc14: e30\n x1 ==2,3<=x2<4
loc15 -right-> loc16: e31\n x1 ==3,3<=x2<4
loc16 -left-> loc15: e32\n x1 ==3,3<=x2<4
@enduml
