search

UoY-RoboStar / robocert-textual

Textual plugin and CSP generator for RoboCert
Eclipse Public License 2.0
2 stars 0 forks source link

Allow lower bound on deadline blocks? #51

Open MattWindsor91 opened 3 years ago

MattWindsor91 commented 3 years ago

It makes sense from a UML perspective for a deadline block to have a lower bound as well as an upper bound, but I'm not entirely sure what the purpose or semantics of this would be. I guess you'd need something like

P |[ can_stop |] (Wait(lb); can_stop -> Skip)) /\ (Wait(ub); UStop)

and this would be something like a budget?

Including this for UML parity, but it may be that we decide not to have it. Also including for PSC parity because I think TPSC can encode this.

MattWindsor91 commented 3 years ago

The syntax would be something like

taking between X and Y units {
}

with deadlines as they are now becoming

taking up to Y units {
}
MattWindsor91 commented 3 years ago

And the metamodel name might have to generalise to DurationStep eg.

MattWindsor91 commented 2 years ago

I've done a bit of CSP inspection to see if I could replace

wait for X units

with

taking between X and X units

with a tentative semantics of

Timed(OneStep) {
        AtLeast(P, n) = P ||| WAIT(n)
        Duration(P, lo, hi) = EndBy(AtLeast(P, lo), hi)
}

There are a few oddities and differences between trace and tick-tock semantics that I haven't quite understood yet, but I'll hopefully work it out.

My understanding too, though, is that it's worth being able to put a minimum/maximum duration on a block local to one lifeline, but also use a wait in action position, and possibly also a deadline across multiple lifelines, and I haven't been able to work out how to reconcile the three.