11.3.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

Commit 5388fd54 authored by Philipp Meyer's avatar Philipp Meyer

Changed snapshot algorithm to synchronous communication

parent 6cbee54f
petri net "snapshot 2" {
places {
white1 red1 received1 notreceived1 sent1 notsent1 marker1 sample1 done1
white2 red2 received2 notreceived2 sent2 notsent2 marker2 sample2 done2
white1 red1 sent1 notsent1 sample1
white2 red2 sent2 notsent2 sample2
}
transitions {
init1 receive_white1 receive_red1 send1
init2 receive_white2 receive_red2 send2
init1 send1white2 send1red2 // comm1white comm1red
init2 send2white1 send2red1 // comm2white comm2red
snapshot
reset1
reset2
}
arcs {
// white1 -> comm1white -> white1
// { red1, sent1 } -> comm1red -> { red1, sent1 }
white1 -> init1 -> { red1, sample1 }
{ white1, notreceived1, marker2 } -> receive_white1 -> { red1, received1, sample1 }
{ red1, notreceived1, marker2 } -> receive_red1 -> { red1, received1 }
{ red1, notsent1 } -> send1 -> { red1, sent1, marker1 }
{ red1, notsent1, white2 } -> send1white2 -> { red1, sent1, red2, sample2 }
{ red1, notsent1, red2 } -> send1red2 -> { red1, sent1, red2 }
// white2 -> comm2white -> white2
// { red2, sent2 } -> comm2red -> { red2, sent2 }
white2 -> init2 -> { red2, sample2 }
{ white2, notreceived2, marker1 } -> receive_white2 -> { red2, received2, sample2 }
{ red2, notreceived2, marker1 } -> receive_red2 -> { red2, received2 }
{ red2, notsent2 } -> send2 -> { red2, sent2, marker2 }
{ red2, notsent2, white2 } -> send2white1 -> { red2, sent2, red1, sample1 }
{ red2, notsent2, red1 } -> send2red1 -> { red2, sent2, red1 }
{ sample1, sample2 } -> snapshot -> { done1, done2 }
{ red1, done1, received1, sent1 } -> reset1 -> { white1, notreceived1, notsent1 }
{ red2, done2, received2, sent2 } -> reset2 -> { white2, notreceived2, notsent2 }
{ sample1, sample2, red1, red2, sent1, sent2 } -> snapshot -> { white1, white2, notsent1, notsent2 }
}
initial {
white1 notreceived1 notsent1
white2 notreceived2 notsent2
white1 notsent1
white2 notsent2
}
}
liveness property {
......
Markdown is supported
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