|Summary:||Relax restriction: clock guards are not allowed on broadcast receivers|
|Product:||UPPAAL||Reporter:||Timothy Bourke <tbourke>|
|Component:||Engine||Assignee:||Alexandre David <adavid>|
Description Timothy Bourke 2008-01-31 05:48:54 CET
Allowing clock guards on broadcast receivers is a natural generalization of Uppaal's semantics, and a useful feature for certain types of trace inclusion testing. Date: Sun, 13 Jan 2008 09:54:58 +1100 From: Timothy Bourke <email@example.com> To: firstname.lastname@example.org Subject: Re: [UPPAAL] Clock guards are not allowed on broadcast receivers On Jan 12 at 14:39 +0100, Marius Mikucionis wrote: > 2008/1/12, timothybourke <email@example.com>: > > Broadcast channels are useful but the restriction on receiver clock > > guards is limiting. > > Yes. But I think it is also quite unnatural to have guards on receiving edges. > An motivating example would be nice. Also a description is needed > about what you expect to happen. There are two models: T a timing diagram modelled as a timed automaton. D || S a driver connected to a hardware sensor, modelled as two communicating timed automata. The communication between D and S should refine, in terms of timed trace inclusion, the protocol specified in T. To validate this, I construct a testing automaton T' by `inverting' T using the technique described individually by Jensen and Stoelinga (and suggested to me by Prof. Vaandrager): D || S || T' |= A not T'.Err implies ABS(D || S) <=tr T where ABS abstracts from signals not in T. In this case, broadcast channels are useful because 1) Each component is automatically input-enabled, and, 2) The tester T' can unobtrusively check the protocol (as a synchronous observer would). Due to the testing construction, any location invariant in T becomes a transition guard in T', and then the restriction on broadcast inputs is limiting. (Note: Broadcast outputs are not directly useful in the testing construction because whether they occur or not says nothing about the behaviour of the system being tested. Thus the construction of T', and the application of the testing technique is non-standard.) I can do the testing without broadcast channels by splitting each channel C into three: DC, C, SC; and adding an intermediate automaton: (I) --DC?--> (C) --C!--> (C) /\ | | | +--------SC!------------+ where (I) is an initial state, and (C) a committed state. But extra care is required to preserve the input-enabled property of each component, and the model is more complicated. > If you just want a different receiving behavior depending on time, > then receive synchronization into urgent location and then have > several outgoing edges with guards that you want. Yes, having different receiving behaviour depending on time is the key requirement. Your suggestion seems a good one. I hadn't thought of it. > > Perhaps it would be intricate to implement, or costly to validate? > > I see that the problem has two sides: semantical and implementation > (performance). > > Semantically, the receiving edges in the broadcast synchronization > either participate or not. If there are no receiving edges (or all > guards are false), the shouting edge will still be executed anyway, > hence this is a one to zero-or-many communication. If you put timing > constraints (clock guards) then it is not clear how to execute it: > should the result be a conjunction of guards (this would modify the > senders clock values and violate the one-to-zero communication > possibility)? a disjunction? something else? > In case of disjunction or else, there is a potential exponential > blow-up: we will need to consider all possible combinations of > receiving edges multiplied by number of bounds dictated by guards. And > this is probably the last thing you want. I see clock guards on receivers as a natural generalization. A location with no outgoing edges for inputs on a particular channel does not inhibit output on that channel. Neither should a state (location * variable values * clock value) with no outgoing transitions for input on a particular channel. > Implementation wise. The problem is that UPPAAL looks at the > communicating edges and decides which receiving edges participate and > which do not. If you put guards on those edges it means that UPPAAL > have to evaluate them. This does not pose much problem for integer > guards as they don't modify the state, however the clock guards modify > the symbolic state, which means UPPAAL will have to make a copy of a > symbolic state for each potential edge, evaluate it just to determine > whether edge is participating in the communication and then discard > it. This not just complicates things, but it would also put > significant performance penalty (state copy is quite expensive). Thank you for the explanation. I don't have a good grasp of the algorithms. If it would be costly, than I can just as well use my existing work-around or the alternative you have suggested. > > Should I post an enhancement suggestion (to Bugzilla)? > > I don't see a reason why not. If you have enough motivating example, > maybe this feature has a future :-) Ok. I'll think about it all for a bit longer. If I do post a suggestion, I'll include extracts from this discussion. Please do let me know if the example requires clarification. Thank you, Tim.