in discussion Finite State Processes (FSP) / Questions » railway signaling systems
Hello everyone. I have a question regarding FSP. My goal is to model a rail system and I have as main actors: the cabin of train control and signaling system to the ground. I wrote this code FSP, but it is all in a single process called ENGINE how do I separate them? I want to do this to enable the display of graphics LTS (I have been too many to view them with LTSA) and exploit the potential of the tool that allows concurrent software
Here is the code FSP:
const MAX_DIST = 5
range DIST = 0..MAX_DIST
const MAX_SEC = 12
range SEC = 0..MAX_SEC
const MAX_VEL = 5
range VEL = 1..MAX_VEL
ENGINE = (engineOn ->THROTTLE),
THROTTLE = ( start -> SPEED_COUNTER[1]
| engineOff ->ENGINE
),
SPEED_COUNTER[v:VEL] = ( when(v<MAX_VEL) accelerator[v] ->SPEED_COUNTER[v+1]
| when(v>1) reduceSpeed[v-1] ->SPEED_COUNTER[v-1]
| engineOff ->ENGINE
| when(v>1) signal_received ->metri250->DISTANCE[MAX_DIST][v]
| csr ->beep->CSR[v][MAX_SEC]
),
CSR[v:VEL][s:SEC] =
(when(s>0)tick->CSR[v][s-1]
|when(s==0) brake->SPEED_COUNTER[1]
|when(s>0)release -> CHECK_DISTANCE[MAX_DIST][v]
|signal_received -> release -> SPEED_COUNTER[v]
),
DISTANCE[d:DIST][v:VEL] =
(when(d>0)avanza50mt->DISTANCE[d-1][v]
|when(d==0) brake->SPEED_COUNTER[1]
|when(d>0)csr ->beep->CSR[v][MAX_SEC]
),
CHECK_DISTANCE[c:DIST][v:VEL] =
(when(c>0)avanza50mt->CHECK_DISTANCE[c-1][v]
|when(c==0) brake->SPEED_COUNTER[1]
|when(c>0) signal_received ->SPEED_COUNTER[v]
).
Thanks for any reply if you need more information contact me.
Sincerely Stefano