Bug 436

Summary: Relax restriction: clock guards are not allowed on broadcast receivers
Product: UPPAAL Reporter: Timothy Bourke <tbourke>
Component: EngineAssignee: Alexandre David <adavid>
Status: ASSIGNED ---    
Severity: enhancement    
Priority: P2    
Version: 4.0.6   
Hardware: All   
OS: All   
URL: http://tech.groups.yahoo.com/group/uppaal/message/1401?var=0&l=1
Architecture:

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 <timbob@bigpond.com>
To: uppaal@yahoogroups.com
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 <timbob@bigpond.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.