You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
3527 lines
127 KiB
3527 lines
127 KiB
|
|
{
|
|
"jani-version":1,
|
|
"features":[
|
|
"derived-operators"
|
|
],
|
|
"name":"Converted from PRISM by IscasMC",
|
|
"type":"pta",
|
|
"actions":[
|
|
{
|
|
"name":"snd_req12"
|
|
},
|
|
{
|
|
"name":"snd_ack12"
|
|
},
|
|
{
|
|
"name":"snd_idle12"
|
|
},
|
|
{
|
|
"name":"rec_req12"
|
|
},
|
|
{
|
|
"name":"rec_ack12"
|
|
},
|
|
{
|
|
"name":"rec_idle12"
|
|
},
|
|
{
|
|
"name":"rec_idle21"
|
|
},
|
|
{
|
|
"name":"rec_req21"
|
|
},
|
|
{
|
|
"name":"rec_ack21"
|
|
},
|
|
{
|
|
"name":"loop"
|
|
},
|
|
{
|
|
"name":"snd_req21"
|
|
},
|
|
{
|
|
"name":"snd_ack21"
|
|
},
|
|
{
|
|
"name":"snd_idle21"
|
|
}
|
|
],
|
|
"constants":[
|
|
{
|
|
"name":"delay",
|
|
"type":"int"
|
|
}
|
|
],
|
|
"variables":[
|
|
{
|
|
"name":"w12",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":9
|
|
}
|
|
},
|
|
{
|
|
"name":"y1",
|
|
"type":"clock"
|
|
},
|
|
{
|
|
"name":"y2",
|
|
"type":"clock"
|
|
},
|
|
{
|
|
"name":"x1",
|
|
"type":"clock"
|
|
},
|
|
{
|
|
"name":"s1",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":8
|
|
}
|
|
},
|
|
{
|
|
"name":"w21",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":9
|
|
}
|
|
},
|
|
{
|
|
"name":"z1",
|
|
"type":"clock"
|
|
},
|
|
{
|
|
"name":"z2",
|
|
"type":"clock"
|
|
},
|
|
{
|
|
"name":"x2",
|
|
"type":"clock"
|
|
},
|
|
{
|
|
"name":"s2",
|
|
"type":{
|
|
"kind":"bounded",
|
|
"base":"int",
|
|
"lower-bound":0,
|
|
"upper-bound":8
|
|
}
|
|
}
|
|
],
|
|
"observables":[
|
|
{
|
|
"name":"\"time\""
|
|
},
|
|
{
|
|
"name":"\"time_sending\""
|
|
}
|
|
],
|
|
"initial-states":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"w12",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"y1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"y2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"w21",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"z1",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"z2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"x2",
|
|
"right":0
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"=",
|
|
"left":"s2",
|
|
"right":0
|
|
}
|
|
}
|
|
},
|
|
"automata":[
|
|
{
|
|
"name":"wire12",
|
|
"locations":[
|
|
{
|
|
"name":"location",
|
|
"observables":[
|
|
{
|
|
"ref":"\"time\"",
|
|
"value":1
|
|
},
|
|
{
|
|
"ref":"\"time_sending\"",
|
|
"value":{
|
|
"op":"?:",
|
|
"args":[
|
|
{
|
|
"op":"∨",
|
|
"left":{
|
|
"op":">",
|
|
"left":"w12",
|
|
"right":0
|
|
},
|
|
"right":{
|
|
"op":">",
|
|
"left":"w21",
|
|
"right":0
|
|
}
|
|
},
|
|
1,
|
|
0
|
|
]
|
|
}
|
|
}
|
|
],
|
|
"invariant":{
|
|
"exp":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"∧",
|
|
"left":{
|
|
"op":"⇒",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"w12",
|
|
"right":1
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":"y2",
|
|
"right":"delay"
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"⇒",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"w12",
|
|
"right":2
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":"y1",
|
|
"right":"delay"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"⇒",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"w12",
|
|
"right":3
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":"y2",
|
|
"right":"delay"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"⇒",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"w12",
|
|
"right":4
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":"y1",
|
|
"right":"delay"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"⇒",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"w12",
|
|
"right":5
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":"y2",
|
|
"right":"delay"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"⇒",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"w12",
|
|
"right":6
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":"y1",
|
|
"right":"delay"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"⇒",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"w12",
|
|
"right":7
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":"y1",
|
|
"right":"delay"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"⇒",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"w12",
|
|
"right":8
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":"y1",
|
|
"right":"delay"
|
|
}
|
|
}
|
|
},
|
|
"right":{
|
|
"op":"⇒",
|
|
"left":{
|
|
"op":"=",
|
|
"left":"w12",
|
|
"right":9
|
|
},
|
|
"right":{
|
|
"op":"≤",
|
|
"left":"y1",
|
|
"right":"delay"
|
|
}
|
|