lf-lang / lingua-franca

Intuitive concurrent programming in any language
https://www.lf-lang.org
Other
231 stars 62 forks source link

Clock keyword #20

Closed lhstrh closed 5 years ago

lhstrh commented 5 years ago

We've been getting some feedback that the clock keyword causes confusion. The keyword is syntactic sugar for specifying future events (without invoking schedule in a reaction). As an alternative, timer has been mentioned, but that seems to fail to capture the potentially periodic nature of the events it prescribes to occur. Thoughts?

MarjanSirjani commented 5 years ago

What are the objections to using “clock”?

How would you write the clock c(p) (or better say reaction(c)) in the Ramp example using schedule? (want to see the exact syntax.)

On 19 Apr 2019, at 02:47, Marten Lohstroh notifications@github.com<mailto:notifications@github.com> wrote:

We've been getting some feedback that the clock keyword causes confusion. The keyword is syntactic sugar for specifying future events (without invoking schedule in a reaction). As an alternative, timer has been mentioned, but that seems to fail to capture the potentially periodic nature of the events it prescribes to occur. Thoughts?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7Cadca53cf0e5745696f7708d6c44baebe%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636912226676047819&sdata=iAfHU%2FHMZuqBK8uD4UeO1LegxzVpIfLfAKpEGJkhjxY%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYBXW2VX3IMIDKMNIV3PRDXQRANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7Cadca53cf0e5745696f7708d6c44baebe%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636912226676057828&sdata=ECEUM9JWk2WFos1jU1TjxhI%2BLwNOfNXbUjfT6tSaMj4%3D&reserved=0.

lhstrh commented 5 years ago

It apparently leads people to believe that reactors have their own clock and thus are asynchronous from other reactors/clocks. Clocks are syntactic sugar because everything can be done with actions. For instance:

reactor PeriodicHello() {
action a(5 ms);
output o:string;

constructor() {
  this.schedule(a);
}

reaction(a) -> o
  o.set("hello");
  this.schedule(a);
}

with the clock keyword, this would look like:

reactor PeriodicHello() {
clock c(5 ms);
output o:string;

reaction(c) -> o
  o.set("hello");
}

In other words, the calls to schedule are implied in the latter example. The idea now is to consider an alternative keyword that better captures its meaning.

edwardalee commented 5 years ago

I have an idea that might unify several concepts, reducing three keyword to one. Specifically, we can have:

reactor PeriodicHello(...) { schedule doIt(offset, period); output o:string; reaction(doIt) { set(o, ‘hello’); } }

The meaning of the arguments is as follows:

offset: The start time, or TRIGGERED to specify no start time. period: The period, or ONCE to specify to trigger only once.

The default, if the arguments are not given, is TRIGGERED, ONCE. This makes the “action” keyword unnecessary.

Then, in any reaction, one can do:

reaction(...) -> doIt { ... schedule(doIt, offset, period)); ... }

The reaction declares that it triggers doIt so that doIt will be in scope and so that dependencies can be analyzed (there is always at least one microstep delay, however).

The meanings of the second and third arguments (both optional) are:

offset: Additional offset, over and above that given in the doIt schedule declaration. Must be nonnegative. The action will be scheduled

period: Increment to the period, over and above the period given in the doIt schedule declaration, or STOP to specify that no more triggerings should occur.

Whenever schedule() is called in a reaction, if the named schedule is already active, then at the time specified (always at least one microsecond later), the active schedule will be replaced by the new one.

There are several usage patterns:

  1. Simple periodic action.
  2. Action taken upon starting the execution (making the keyword “initialize” unnecessary).
  3. Constant delay actor.
  4. Variable delay actor with a static minimum delay (useful for PTIDES).
  5. Asynchronous callback that triggers a one time reaction.
  6. Asynchronous callback that starts or stops a periodic reaction.
  7. Reaction that changes the period of a periodic reaction (but never making it less than the declared period).
  8. Sporadic sensor.

The last one is the most interesting. A sporadic sensor with a minimum interarrival time of 10 would be specified as follows:

reactor Sensor(...) { schedule sense(TRIGGERED, 10); schedule start(0); // default second argument is ONCE. output data; ... } reaction(start) -> sense { ... set up sensor, giving it callback function() { ... get sensor data and store it in a state variable... schedule(sense, 0); // default third argument is ONCE. } }

reaction(sense) -> data { set(data, state variable value); }

The above could be implemented with any of the following semantics:

  1. If the callback gets invoked more often than every 10 time units, sensor values are overwritten and not passed to the data output (this is what the code sketch above does).

  2. If the callback gets invoked too often, sensor values could be queued. This is dangerous, of course, as it may require unbounded memory.

  3. If the callback occurs too often, an error condition could be raised, eg. By producing an error output, causing the model to adapt.

Edward


Edward A. Lee EECS, UC Berkeley eal@eecs.berkeley.edu http://eecs.berkeley.edu/~eal

On Apr 19, 2019, at 11:20 AM, Marten Lohstroh notifications@github.com wrote:

It apparently leads people to believe that reactors have their own clock and thus are asynchronous from other reactors/clocks. Clocks are syntactic sugar because everything can be done with actions. For instance:

reactor PeriodicHello() { action a(5 ms); output o:string;

constructor() { this.schedule(a); }

reaction(a) -> o o.set("hello"); this.schedule(a); } with the clock keyword, this would look like:

reactor PeriodicHello() { clock c(5 ms); output o:string;

reaction(c) -> o o.set("hello"); } In other words, the calls to schedule are implied in the latter example. The idea now is to consider an alternative keyword that better captures its meaning.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

MarjanSirjani commented 5 years ago

I am not sure I understand everything, but I like what I understood. I don’t like syntactic sugar, and I like least keywords possible. I think what you are proposing is intuitive enough.

lhstrh commented 5 years ago

I think the action is an important construct that doesn't seem to be a good idea to make implicit. For the handling of asynchronous callbacks, for instance, I may not want to schedule anything until the time that the callback is invoked. In that case, I would like to simply declare an action (not a clock or a schedule). I also find it somewhat confusing that in the proposal there are two distinct entities that are called schedule, namely, the declaration of a schedulable action and the schedule function that can be invoked inside of reactions.

As we're working on the formalization of reactors, we're actually finding that "actions" play a key role in definition the semantics of composites...

Unlike Marjan, I do like syntactic sugar because it reuses core programming constructs rather than require the introduction of new ones. Therefore, I don't generally see it as a goal to reduce the number of keywords.

I also like the idea of centering our discussions around a list of interesting usage patterns, but it looks like we should also be able to handle them with the existing syntax. Or am I missing something?

edwardalee commented 5 years ago

You might want to look more closely. I don’t think my proposal changes the “action” semantics in any significant way except to change the keyword to “schedule” (and to generalize to allow periodicity). We could keep the keyword “action”, but I actually think “schedule” may be clearer.

Edward


Edward A Lee Professor UC Berkeley

On Apr 21, 2019, at 12:36 PM, Marten Lohstroh notifications@github.com wrote:

I think the action is an important construct that doesn't seem to be a good idea to make implicit. For the handling of asynchronous callbacks, for instance, I may not want to schedule anything until the time that the callback is invoked. In that case, I would like to simple declare an action (not a clock or a schedule). I also find it somewhat confusing that in the proposal there are two distinct entities that are called schedule, namely, the declaration of a schedulable action and the schedule function that can be invoked inside of reactions.

As we're working on the formalization of reactors, we're actually finding that "actions" play a key role in definition the semantics of composites...

Unlike Marjan, I do like syntactic sugar because it reuses core programming constructs rather than require the introduction of new ones. Therefore, I don't generally see it as a goal to reduce the number of keywords.

I also like the idea of centering our discussions around a list of interesting usage patterns, but it looks like we should also be able to handle them with the existing syntax. Or am I missing something?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/icyphy/lingua-franca/issues/20#issuecomment-485265212, or mute the thread https://github.com/notifications/unsubscribe-auth/ACA6ONSJEVSPLLCFWLVJF53PRSJZBANCNFSM4HHAWV4Q .

MarjanSirjani commented 5 years ago

Now that you are working on formalisation of reactors maybe at some point you can tell me the differences between reactions and message servers in Timed Rebeca at the semantics level and why you need to distinguish actions.

Side note: "syntactic sugar is syntax within a programming language that is designed to make things easier to read or to express. It makes the language "sweeter" for human use: things can be expressed more clearly, more concisely, or in an alternative style that some may prefer." I don’t like to allow “alternative style”. I think it may increase complexity.

On 21 Apr 2019, at 21:06, Marten Lohstroh notifications@github.com<mailto:notifications@github.com> wrote:

I think the action is an important construct that doesn't seem to be a good idea to make implicit. For the handling of asynchronous callbacks, for instance, I may not want to schedule anything until the time that the callback is invoked. In that case, I would like to simple declare an action (not a clock or a schedule). I also find it somewhat confusing that in the proposal there are two distinct entities that are called schedule, namely, the declaration of a schedulable action and the schedule function that can be invoked inside of reactions.

As we're working on the formalization of reactors, we're actually finding that "actions" play a key role in definition the semantics of composites...

Unlike Marjan, I do like syntactic sugar because it reuses core programming constructs rather than require the introduction of new ones. Therefore, I don't generally see it as a goal to reduce the number of keywords.

I also like the idea of centering our discussions around a list of interesting usage patterns, but it looks like we should also be able to handle them with the existing syntax. Or am I missing something?

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20%23issuecomment-485265212&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C826d6a0f8c4d417f3d1008d6c6778416%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636914614369233824&sdata=eTp9pUFAR5Pd4VoKr4OsrhTkDql2Kt1nVE3lvMatYKQ%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYDQNEMFVJ5XA6IHX2TPRSJZBANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C826d6a0f8c4d417f3d1008d6c6778416%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636914614369243828&sdata=gaV6fVaqIZowyvlCIji%2BBENGYmo9cxu3Tl0C9CPNyfo%3D&reserved=0.

lhstrh commented 5 years ago

After having a closer look, I see that you did cover the canonical action case. It wasn't obvious to me. We used to have:

action sense(10 ms);
clock start(0, 0, 1);

You're proposing:

schedule sense(TRIGGERED, 10);
schedule start(0);  // default second argument is ONCE.

Looking at this, I find the first style of declaring "sense" much clearer. In our writings and discussions, we have use the term "trigger" to mean the immediate cause of a reaction. In your proposal this gets overloaded with another meaning: a triggering that occurs in an asynchronous callback (subsequently leading to the triggering of a reaction) -- I find this confusing.

The declaration of "start", on the other hand, looks better in the second piece of code, but we can easily solve that by introducing another keyword, e.g.:

action sense(10 ms);
init start;

I think it's a lot easier to remember the meaning of a keyword than it is to remember the meaning, associated constants, and position of function arguments.

edwardalee commented 5 years ago

Hmm... I'm not sure I agree. The meaning of the first argument is an offset from the "current time" at which reactions should be scheduled. When these are part of a static declaration, "current time" is zero, so the TRIGGERED value says "don't schedule reactions relative to current time; instead, wait until I tell you."

I find it pretty logical and consistent.

Edward

On 4/21/19 11:32 AM, Marten Lohstroh wrote:

After having a closer look, I see that you did cover the canonical |action| case. It wasn't obvious to me. We used to have:

|action sense(10 ms); clock start(0, 0, 1); |

You're proposing:

|schedule sense(TRIGGERED, 10); schedule start(0); // default second argument is ONCE. |

Looking at this, I find the first style of declaring "sense" much clearer. In our writings and discussions, we have use the term "trigger" to mean the immediate cause of a reaction. In your proposal this gets overloaded with another meaning: a triggering that occurs in an asynchronous callback (subsequently leading to the triggering of a reaction) -- I find this confusing.

The declaration of "start", on the other hand, looks better in the second piece of code, but we can easily solve that by introducing another keyword, e.g.:

|action sense(10 ms); init start; |

I think it's a lot easier to remember the meaning of a keyword than it is to remember the meaning, associated constants, and position of function arguments.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/icyphy/lingua-franca/issues/20#issuecomment-485272735, or mute the thread https://github.com/notifications/unsubscribe-auth/ACA6ONR5KTIHQMMSCM5HNILPRSXMPANCNFSM4HHAWV4Q.

-- Edward A. Lee Professor of the Graduate School and Robert S. Pepper Distinguished Professor Emeritus EECS Department, UC Berkeley http://ptolemy.eecs.berkeley.edu/~eal

edwardalee commented 5 years ago

Also, I suggest that you look at all seven design patterns... All are useful. How would you specify them?

Edward

On 4/21/19 11:32 AM, Marten Lohstroh wrote:

After having a closer look, I see that you did cover the canonical |action| case. It wasn't obvious to me. We used to have:

|action sense(10 ms); clock start(0, 0, 1); |

You're proposing:

|schedule sense(TRIGGERED, 10); schedule start(0); // default second argument is ONCE. |

Looking at this, I find the first style of declaring "sense" much clearer. In our writings and discussions, we have use the term "trigger" to mean the immediate cause of a reaction. In your proposal this gets overloaded with another meaning: a triggering that occurs in an asynchronous callback (subsequently leading to the triggering of a reaction) -- I find this confusing.

The declaration of "start", on the other hand, looks better in the second piece of code, but we can easily solve that by introducing another keyword, e.g.:

|action sense(10 ms); init start; |

I think it's a lot easier to remember the meaning of a keyword than it is to remember the meaning, associated constants, and position of function arguments.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/icyphy/lingua-franca/issues/20#issuecomment-485272735, or mute the thread https://github.com/notifications/unsubscribe-auth/ACA6ONR5KTIHQMMSCM5HNILPRSXMPANCNFSM4HHAWV4Q.

-- Edward A. Lee Professor of the Graduate School and Robert S. Pepper Distinguished Professor Emeritus EECS Department, UC Berkeley http://ptolemy.eecs.berkeley.edu/~eal

goens commented 5 years ago

Assuming the semantics are preserved, the proposal seems to be pretty elegant, as it unifies things into a single concept. I do agree it's a bit confusing with difference between the declaration in the reactor: schedule dolt(offset, period); and the actual scheduling within a reaction rule: schedule (dolt,offset,period);

Couldn't the first one just be called action (or any other keyword for that matter) and then schedule takes an action identifier as the first argument? At any case, I don't see exactly where the disagreement seems to be? Why can't we have Edward's proposal define the 'core' language syntax and have some syntactic sugar like init, etc on top of that? By the way, ONCE, TRIGGERED and STOP could also be syntactic sugar for 'null' in this context, too. In the end, having no period is the same as executing once, having no (specified) start time is the same as having to wait to be triggered, etc.

I have a few questions about the proposal though: why would the schedule within the reaction just be able to add additional time to the offset/period? I think that is confusing. Is there a compelling reason why we don't want to allow making periods/offsets shorter than declared)? At least for the offset I see really no reason why. Would these values have to be known at compile time? If so, we could let the syntax specify the absolute values (e.g. PERIOD be the absolute period, not the value to be added to the declared PERIOD) and check at compile time that it does not violate anything (e.g. be non-negative or break any guarantees we could have had).

At any case, I'm having a hard time understanding precisely that the proposal doesn't change the semantics, since I have yet to see a proposed semantics for the timing aspect of the language. I'd think it'd be easier to first settle on the semantics and then decide how best to find a syntax for that.

edwardalee commented 5 years ago

Yes, we could use "action" for the first one and "schedule" for the second. I like that suggestion.

The reason for adding time to the offset or period rather than just setting them is that in both cases, to do real-time analysis, we need to specify a minimum offset and period. The nice feature of my proposal is that the minimum is specified statically, in the LF code, not in the target code, so it can be checked statically and enforced at runtime even without analyzing the target language.

To understand why we need the minimum, consider the question of whether real-time deadlines can be met. Suppose you have a periodic action with period P and the target code can change P to whatever it wants. There is always a small enough value of P such that no real-time constraints can be met because no processor will be able to deliver that small period. Suppose, for example, I change P to be 1 ns, specifying that I want some reaction invoked every nanosecond...

When I said the proposal doesn't change the semantics, I meant that it subsumed at least my understanding of what we had previously proposed for action, clock, and schedule. It also avoids the problematic "clock" keyword.

Edward

On 4/21/19 1:42 PM, goens wrote:

Assuming the semantics are preserved, the proposal seems to be pretty elegant, as it unifies things into a single concept. I do agree it's a bit confusing with difference between the declaration in the reactor: |schedule dolt(offset, period);| and the actual scheduling within a reaction rule: |schedule (dolt,offset,period);|

Couldn't the first one just be called |action| (or any other keyword for that matter) and then |schedule| takes an |action| identifier as the first argument? At any case, I don't see exactly where the disagreement seems to be? Why can't we have Edward's proposal define the 'core' language syntax and have some syntactic sugar like init, etc on top of that? By the way, ONCE, TRIGGERED and STOP could also be syntactic sugar for 'null' in this context, too. In the end, having no period is the same as executing once, having no (specified) start time is the same as having to wait to be triggered, etc.

I have a few questions about the proposal though: why would the |schedule| within the reaction just be able to add additional time to the offset/period? I think that is confusing. Is there a compelling reason why we don't want to allow making periods/offsets shorter than declared)? At least for the offset I see really no reason why. Would these values have to be known at compile time? If so, we could let the syntax specify the absolute values (e.g. PERIOD be the absolute period, not the value to be added to the declared PERIOD) and check at compile time that it does not violate anything (e.g. be non-negative or break any guarantees we could have had).

At any case, I'm having a hard time understanding precisely that the proposal doesn't change the semantics, since I have yet to see a proposed semantics for the timing aspect of the language. I'd think it'd be easier to first settle on the semantics and then decide how best to find a syntax for that.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/icyphy/lingua-franca/issues/20#issuecomment-485281060, or mute the thread https://github.com/notifications/unsubscribe-auth/ACA6ONRHU77N6QOREUVVEO3PRTGSJANCNFSM4HHAWV4Q.

-- Edward A. Lee Professor of the Graduate School and Robert S. Pepper Distinguished Professor Emeritus EECS Department, UC Berkeley http://ptolemy.eecs.berkeley.edu/~eal

lhstrh commented 5 years ago

I'm working on the list of the examples.

In the meantime, it looks like we're going back to the discussion we had in Issue #4. There, my proposal was also to have the delay associated with an action (if it is static) be declared at the LF level. The only semantic difference here is that I meant for that delay to be an exact delay, whereas you suggest it be interpreted as a minimum delay. I think both are useful; the former to achieve synchronous exchanges, the latter for meeting deadlines.

Should we want both?

MarjanSirjani commented 5 years ago

Would you please let me know if I understood correctly? We are talking about “triggering” reactions in different ways because of receiving some event, right? So, you are defining different "event types”. You defined input, clock, and action (taken from the paper). Now you removed clock and kept input and action.

How is “action” different from other type(s) of events? Can we have just one keyword (for example “Trigger”) instead of Edward’s “Schedule” that cover all types of events in the “core” language?

I am actually repeating Edward’s suggestion, but I am suggesting Trigger because it sounds more general than Schedule. Then we have offset and period as optional parameters of “Trigger” like Edward’s suggestion for Schedule.

I like the suggestion of “geons" (I cannot see the name) of a (lean) core language, and then optional sugar.

Maybe if you explain why “action” is a different type of event to deserve a different name then I understand better.

**From the paper: Events—Messages sent from one reactor to another, and clock and action events each have a timestamp, a value on a logical time line. These are timestamped events that can trigger reactions. Each port, clock, and action can have at most one such event at any logical time. An event may carry a value that will be passed as an argument to triggered reactions.

On 22 Apr 2019, at 03:43, Marten Lohstroh notifications@github.com<mailto:notifications@github.com> wrote:

I'm working on the list of the examples.

In the meantime, it looks like we're going back to the discussion we had in Issue #4https://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F4&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C62839d174c094da9d19508d6c6af088d%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636914852398047934&sdata=o4UTw0Jxl2liIAaZ%2F09NYsg4NO4d%2BIkxo7SQxbyjmI4%3D&reserved=0. There, my proposal was also to have the delay associated with an action (if it is static) be declared at the LF level. The only semantic difference here is that I meant for that delay to be an exact delay, whereas you suggest it be interpreted as a minimum delay. I think both are useful; the former to achieve synchronous exchanges, the latter for meeting deadlines.

Should we want both?

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20%23issuecomment-485289360&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C62839d174c094da9d19508d6c6af088d%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636914852398057938&sdata=rm1t6JxqGJWKW1r2mCPRQ6N7iXjp%2FHW9MhCKV1tUohg%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYDQ2F7ZFNK4OPE7AN3PRTYLJANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C62839d174c094da9d19508d6c6af088d%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636914852398057938&sdata=jeqe39NJBzsEWCHUdkIcJbxc9pHkyFIfb4S1ijBw1b0%3D&reserved=0.

edwardalee commented 5 years ago

Right now, I don’t see a need to know about exact delays for any static analysis. Do you? At run time, exact delays are achievable... the only question is whether they need to be statically declared (and enforced).

But as I was looking at how to implement my proposal, it seems there is still an ambiguity, because for a delay, we want non-zero offset, but also don’t want the action to self trigger. So the offset parameter alone cannot specify both the offset and whether the action self triggers or whether it is triggered by something occurring in a reaction or callback.

So I think it’s best to go back to two keywords. We originally had “action” and “clock”, where “clock” self triggers, and “action” is initiated by a call to “schedule”.

Maybe “clock” could be replaced with “timer”?

Also, I would like to propose that action have two optional arguments, minimumOffset and minimumPeriod, which default to 0 and -1 (ONCE). This way, schedule() could used to start and stop periodic actions.

Edward


Edward A. Lee EECS, UC Berkeley eal@eecs.berkeley.edu http://eecs.berkeley.edu/~eal

On Apr 21, 2019, at 7:13 PM, Marten Lohstroh notifications@github.com wrote:

I'm working on the list of the examples.

In the meantime, it looks like we're going back to the discussion we had in Issue #4. There, my proposal was also to have the delay associated with an action (if it is static) be declared at the LF level. The only semantic difference here is that I meant for that delay to be an exact delay, whereas you suggest it be interpreted as a minimum delay. I think both are useful; the former to achieve synchronous exchanges, the latter for meeting deadlines.

Should we want both?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

ChadliaJerad commented 5 years ago

I think that the confusing keyword is action, rather than clock. It sounds more like a behavior or something equivalent to a reaction.

What about changing action with signal or event? It seems a better fit to what is described in the paper (Please correct me if I am wrong).

clock or timer or alarm do all let you think about self triggered events (and consequently reactions). We just have to choose. timedEvent can also work, but it is too long...

lhstrh commented 5 years ago

Right now, I don’t see a need to know about exact delays for any static analysis. Do you?

I think that both the maximum and minimum delay are useful. You already made the case for having a minimum delay. The maximum delay can be useful for imposing a deadline (timeout) on an asynchronous activity. If both are set, the reactor will behave like a periodic source (modulo exceptions due to missing deadlines).

At run time, exact delays are achievable... the only question is whether they need to be statically declared (and enforced).

If we can provide automatic exception handling on the basis of such declaration, it is useful. Idem for reordering. I'm still working out the implementation details these use cases.

But as I was looking at how to implement my proposal, it seems there is still an ambiguity, because for a delay, we want non-zero offset, but also don’t want the action to self trigger. So the offset parameter alone cannot specify both the offset and whether the action self triggers or whether it is triggered by something occurring in a reaction or callback.

Right. This is the ambiguity that one of my earlier comments was hinting at.

So I think it’s best to go back to two keywords. We originally had “action” and “clock”, where “clock” self triggers, and “action” is initiated by a call to “schedule”. Maybe “clock” could be replaced with “timer”?

It's the most reasonable alternative to clock I've heard so far, and I cannot think of a better alternative. I really like how action and reaction relate to one other, while, at the same time, we can lump timers, inputs, and actions together in the category of triggers. I think the terminology is pretty solid and intuitive.

Also, I would like to propose that action have two optional arguments, minimumOffset and minimumPeriod, which default to 0 and -1 (ONCE). This way, schedule() could used to start and stop periodic actions.

How about switching the order of the offset and period arguments; I think offset isn't used in many (if not most) cases, and switching the order would remove the need for a superfluous '0' in the declaration. I'm not sure how to conveniently add a maxPeriod and maxOffset -- I'll think about it. One way would be to treat these things as aspects rather than parameters.

MarjanSirjani commented 5 years ago

Very good point Chadlia.

It’s a well established terminology in Automata, events are triggered and cause actions to happen. So, actions are put in the same category of reactions not events.

It seems that Edward and Marten are talking about things that are not explained in the paper and there are places that I don’t exactly understand what they’re talking about.

In the paper three types of events are defined: input, clock (timer), actions Their differences and the criteria for this classification is not clear for me.

And as you mentioned the keywords don’t seem to be the most intuitive ones. Are they: inputEvent internalEvent (action) timerEvent

I don’t know. Specially I don’t know what the action Event is.

On 23 Apr 2019, at 03:20, Chadlia Jerad notifications@github.com<mailto:notifications@github.com> wrote:

I think that the confusing keyword is action, rather than clock. It sounds more like a behavior or something equivalent to a reaction.

What about changing action with signal or event? It seems a better fit to what is described in the paper (Please correct me if I am wrong).

clock or timer or alarm do all let you think about self triggered events (and consequently reactions). We just have to choose. timedEvent can also work, but it is too long...

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20%23issuecomment-485579445&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7Cb1e0411dc4b1444966ad08d6c774f25a%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915702439308320&sdata=oC%2FX%2BS3eOWs8Fb1wH4xBaqkq5QLLnaO%2B9Oh1w4OMeWc%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYBUAUHKMUU6NKYQL5TPRY6MBANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7Cb1e0411dc4b1444966ad08d6c774f25a%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915702439308320&sdata=eUEi3O9%2FqcxCV5JX02gDv%2FZ%2BiqKUDUSarppfSHs9qBk%3D&reserved=0.

lhstrh commented 5 years ago

Interestingly, the core reactor concepts of inputs, outputs, and actions actually map strikingly well to I/O automata. From Wikipedia (emphasis added):

"An I/O automaton models a distributed system component that can interact with other system components. It is a simple type of state machine in which the transitions are associated with named actions."[1] There are three types of actions: input, output, and internal actions. The automaton uses its input and output actions to communicate with its environment, whereas the internal actions are only visible to the automaton itself. Unlike internal and output actions that are selected and carried out by the automaton, the input actions – which simply arrive from the environment - are not under automaton's control.[1]

Note that clocks/timers are not mentioned here; in the reactor model, too, they are mostly syntactic sugar, except for the fact that their declarations also enrich the reactor interface with timing information. Needless to say, reactors themselves can be characterized by a state machine. The nice thing about the decomposition into reactions is that it exposes some of the structure of that state machine to the scheduler.

MarjanSirjani commented 5 years ago

Is an action a type of event?

On 23 Apr 2019, at 08:31, Marten Lohstroh notifications@github.com<mailto:notifications@github.com> wrote:

Interestingly, the core reactor concepts of inputs, outputs, and actions actually map strikingly well to I/O automata. From Wikipediahttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FInput%2Foutput_automaton&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C9de368c5c15f420a93fe08d6c7a05ffe%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915889018046565&sdata=DKu6vi%2Br9CQKnzsKEFPZy5%2FYEu%2FJ7MRqXRSTsWIY%2BrM%3D&reserved=0 (emphasis added):

"An I/O automaton models a distributed system component that can interact with other system components. It is a simple type of state machine in which the transitions are associated with named actions."[1] There are three types of actions: input, output, and internal actions. The automaton uses its input and output actions to communicate with its environment, whereas the internal actions are only visible to the automaton itself. Unlike internal and output actions that are selected and carried out by the automaton, the input actions – which simply arrive from the environment - are not under automaton's control.[1https://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FInput%2Foutput_automaton%23cite_note-lynch1997-1&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C9de368c5c15f420a93fe08d6c7a05ffe%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915889018056575&sdata=1xqJzr57%2Fg0U%2FMtct54ZmLLoyF7dVNuxI5Dx8WJ6Riw%3D&reserved=0]

Note that clocks/timers are not mentioned here; in the reactor model, too, they are mostly syntactic sugar, except for the fact that their declarations also enrich the reactor interface with timing information. Needless to say, reactors themselves can be characterized by a state machine. The nice thing about the decomposition into reactions is that it exposes some of the structure of that state machine to the scheduler.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20%23issuecomment-485635156&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C9de368c5c15f420a93fe08d6c7a05ffe%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915889018066579&sdata=qvrQOf1L95gccT4%2FBpGalnHmzzyC9O16KslWHHPa2vc%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYCR3VQNRECZJQIOZ2LPR2CZZANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C9de368c5c15f420a93fe08d6c7a05ffe%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915889018066579&sdata=u7GrSFnzzQJBoMHR4GGPzDKZY5XTw7ScpkgHpBfOh7o%3D&reserved=0.

edwardalee commented 5 years ago

Good point! The main differences are two, I think:

  1. The model of time. I don’t think this is syntactic sugar... it is a core part of the semantics, with the notion of simultaneity well defined.

  2. The embedding of a target language, rather that the specification of behavior as an automaton.

On the second point, I think that LF 2.0 should support modal models.

Edward


Edward A. Lee EECS, UC Berkeley eal@eecs.berkeley.edu http://eecs.berkeley.edu/~eal

On Apr 23, 2019, at 12:05 AM, MarjanSirjani notifications@github.com wrote:

Is an action a type of event?

On 23 Apr 2019, at 08:31, Marten Lohstroh notifications@github.com<mailto:notifications@github.com> wrote:

Interestingly, the core reactor concepts of inputs, outputs, and actions actually map strikingly well to I/O automata. From Wikipediahttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FInput%2Foutput_automaton&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C9de368c5c15f420a93fe08d6c7a05ffe%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915889018046565&sdata=DKu6vi%2Br9CQKnzsKEFPZy5%2FYEu%2FJ7MRqXRSTsWIY%2BrM%3D&reserved=0 (emphasis added):

"An I/O automaton models a distributed system component that can interact with other system components. It is a simple type of state machine in which the transitions are associated with named actions."[1] There are three types of actions: input, output, and internal actions. The automaton uses its input and output actions to communicate with its environment, whereas the internal actions are only visible to the automaton itself. Unlike internal and output actions that are selected and carried out by the automaton, the input actions – which simply arrive from the environment - are not under automaton's control.[1https://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FInput%2Foutput_automaton%23cite_note-lynch1997-1&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C9de368c5c15f420a93fe08d6c7a05ffe%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915889018056575&sdata=1xqJzr57%2Fg0U%2FMtct54ZmLLoyF7dVNuxI5Dx8WJ6Riw%3D&reserved=0]

Note that clocks/timers are not mentioned here; in the reactor model, too, they are mostly syntactic sugar, except for the fact that their declarations also enrich the reactor interface with timing information. Needless to say, reactors themselves can be characterized by a state machine. The nice thing about the decomposition into reactions is that it exposes some of the structure of that state machine to the scheduler.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20%23issuecomment-485635156&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C9de368c5c15f420a93fe08d6c7a05ffe%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915889018066579&sdata=qvrQOf1L95gccT4%2FBpGalnHmzzyC9O16KslWHHPa2vc%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYCR3VQNRECZJQIOZ2LPR2CZZANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C9de368c5c15f420a93fe08d6c7a05ffe%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915889018066579&sdata=u7GrSFnzzQJBoMHR4GGPzDKZY5XTw7ScpkgHpBfOh7o%3D&reserved=0.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

edwardalee commented 5 years ago

The connection with IO Automata suggests that we could change the keyword “action” to “internal”. Thoughts?

Edward


Edward A. Lee EECS, UC Berkeley eal@eecs.berkeley.edu http://eecs.berkeley.edu/~eal

On Apr 22, 2019, at 10:44 PM, MarjanSirjani notifications@github.com wrote:

Very good point Chadlia.

It’s a well established terminology in Automata, events are triggered and cause actions to happen. So, actions are put in the same category of reactions not events.

It seems that Edward and Marten are talking about things that are not explained in the paper and there are places that I don’t exactly understand what they’re talking about.

In the paper three types of events are defined: input, clock (timer), actions Their differences and the criteria for this classification is not clear for me.

And as you mentioned the keywords don’t seem to be the most intuitive ones. Are they: inputEvent internalEvent (action) timerEvent

I don’t know. Specially I don’t know what the action Event is.

On 23 Apr 2019, at 03:20, Chadlia Jerad notifications@github.com<mailto:notifications@github.com> wrote:

I think that the confusing keyword is action, rather than clock. It sounds more like a behavior or something equivalent to a reaction.

What about changing action with signal or event? It seems a better fit to what is described in the paper (Please correct me if I am wrong).

clock or timer or alarm do all let you think about self triggered events (and consequently reactions). We just have to choose. timedEvent can also work, but it is too long...

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20%23issuecomment-485579445&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7Cb1e0411dc4b1444966ad08d6c774f25a%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915702439308320&sdata=oC%2FX%2BS3eOWs8Fb1wH4xBaqkq5QLLnaO%2B9Oh1w4OMeWc%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYBUAUHKMUU6NKYQL5TPRY6MBANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7Cb1e0411dc4b1444966ad08d6c774f25a%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636915702439308320&sdata=eUEi3O9%2FqcxCV5JX02gDv%2FZ%2BiqKUDUSarppfSHs9qBk%3D&reserved=0. — You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

edwardalee commented 5 years ago

Hmm... I'm not sure about the maximum delay. What would the code look like? It seems like it can't be the LF compiler that imposes the deadline (timeout) on an asynchronous activity. That would have to be the application code. The LF compiler can't possibly know what to do when the time expires. The best it could do would be to generate code that checks that an output is produced before the maximum delay, but what if that output is a reaction to something else? And what would the generated code do if the application code doesn't produce an output?

I don't see a way to make a maximum delay work in LF.

Same for exact delays. I think that building in too much application-specific semantics into LF is a mistake. It greatly complicates the language, and my guess is that very few reactors will need these features. Probably it would be better to enhance LF with inheritance and then build base-class actors that implement these patterns.

Edward

On 4/22/19 4:03 PM, Marten Lohstroh wrote:

Right now, I don’t see a need to know about exact delays for any
static analysis. Do you?

I think that both the maximum and minimum delay are useful. You already made the case for having a minimum delay. The maximum delay can be useful for imposing a deadline (timeout) on an asynchronous activity. If both are set, the reactor will behave like a periodic source (modulo exceptions due to missing deadlines).

At run time, exact delays are achievable... the only question is
whether they need to be statically declared (and enforced).

If we can provide automatic exception handling on the basis of such declaration, it is useful. Idem for reordering. I'm still working out the implementation details these use cases.

But as I was looking at how to implement my proposal, it seems there
is still an ambiguity, because for a delay, we want non-zero offset,
but also don’t want the action to self trigger. So the offset
parameter alone cannot specify both the offset and whether the
action self triggers or whether it is triggered by something
occurring in a reaction or callback.

Right. This is the ambiguity that one of my earlier comments was hinting at.

So I think it’s best to go back to two keywords. We originally had
“action” and “clock”, where “clock” self triggers, and “action” is
initiated by a call to “schedule”. Maybe “clock” could be replaced
with “timer”?

It's the most reasonable alternative to |clock| I've heard so far, and I cannot think of a better alternative. I really like how |action| and |reaction| relate to one other, while, at the same time, we can lump timers, inputs, and actions together in the category of triggers. I think the terminology is pretty solid and intuitive.

Also, I would like to propose that action have two optional
arguments, minimumOffset and minimumPeriod, which default to 0 and
-1 (ONCE). This way, schedule() could used to start and stop
periodic actions.

How about switching the order of the offset and period arguments; I think offset isn't used in many (if not most) cases, and switching the order would remove the need for a superfluous '0' in the declaration. I'm not sure how to conveniently add a |maxPeriod| and |maxOffset| -- I'll think about it. One way would be to treat these things as aspects rather than parameters.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/icyphy/lingua-franca/issues/20#issuecomment-485582590, or mute the thread https://github.com/notifications/unsubscribe-auth/ACA6ONWBD6XZSIDB7BC7TPLPRY747ANCNFSM4HHAWV4Q.

-- Edward A. Lee Professor of the Graduate School and Robert S. Pepper Distinguished Professor Emeritus EECS Department, UC Berkeley http://ptolemy.eecs.berkeley.edu/~eal

lhstrh commented 5 years ago

The connection with IO Automata suggests that we could change the keyword “action” to “internal”. Thoughts? Edward

I thought of this option, too, but I realized it introduces ambiguity because it requires reasoning from a certain perspective for the notion of "internal" to make sense. For instance, an asynchronous callback is often though of something "external" from the perspective of the model, yet it would result in internal actions. Sounds pretty confusing. Another reason to prefer action over internal is that (like the other keywords) action is a noun. Nouns are more easily referenced in text than adjectives.

MarjanSirjani commented 5 years ago

— Events and Reactions; and why callbacks/actions are different?

I understand two general concepts for actors: events and reactions In Timed Rebeca we have message servers that are reactions in LF, and react to events (messages), and messages/events that are sent (triggered and will be served by the receiver).

We can have time-triggered events, or events sent by other actors. See http://rebeca-lang.org/assets/papers/2014/Timed-Rebeca-Shift-Equivalency-published.pdf http://rebeca-lang.org/assets/papers/2014/Modelling%20and%20simulation%20of%20asynchronous%20real-time%20systems%20using%20Timed%20Rebeca.pdf

I don’t understand why you are treating call-backs differently. Would you please explain?

On 23 Apr 2019, at 18:55, Marten Lohstroh notifications@github.com<mailto:notifications@github.com> wrote:

The connection with IO Automata suggests that we could change the keyword “action” to “internal”. Thoughts? Edward

I thought of this option, too, but I realized it introduces ambiguity because it requires reasoning from a certain perspective for the notion of "internal" to make sense. For instance, an asynchronous callback is often though of something "external" from the perspective of the model, yet it would result in internal actions. Sounds pretty confusing. Another reason to prefer action over internal is that (like the other keywords) action is a noun. Nouns are more easily referenced in text than adjectives.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20%23issuecomment-485825561&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C8afdc04da2064001718208d6c7f77e22%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636916263128328234&sdata=nJyx2A6P76dQL%2B7ZRUv5NQUqqLHDSdxZFwXgOV8ho28%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYC4R7O5XU4JYSSDKK3PR4L4LANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C8afdc04da2064001718208d6c7f77e22%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636916263128328234&sdata=CW1uufnuzNbkz1%2FSCpfSCqNLhxrfwnL%2FgyejgRfSfII%3D&reserved=0.

MarjanSirjani commented 5 years ago

— Timed Input Output Transition System (TIOTS) as semantics of DE

We used TIOTS as semantics of our Coordinated Actor Model in http://rebeca-lang.org/assets/papers/2018/Runtime-Compositional-Verification-of-Self-adaptive-Systems.pdf

The paper is not yet published, we sent it to IEEE TSE last Nov. but it got rejected. I sent an older version to Edward last spring (2018). The paper is not easy to read, and I am trying to break it in two, and give the semantics of Magnifier in TIOTS (see figure 2), and semantics of DE as SOS rules (Section 4). I’ll send you a better version when we have one.

Our semantics is based on two papers on Timed I/O Automata (TIOA) and Timed Input Output Transition System (TIOTS) or timed input-output LTS (TIOLTS) in two papers, one by Kim Larsen and other one by Stavros.

Compositional Verification of Real-Time Systems Using Ecdar Alexandre David and Kim. G. Larsen and Axel Legay and Mikael H. Møller and Ulrik Nyman and Anders P. Ravn and Arne Skou and Andrzej Wąsowski

and Conformance Testing for Real-Time Systems Moez Krichen and Stavros Tripakis

On 23 Apr 2019, at 18:55, Marten Lohstroh notifications@github.com<mailto:notifications@github.com> wrote:

The connection with IO Automata suggests that we could change the keyword “action” to “internal”. Thoughts? Edward

I thought of this option, too, but I realized it introduces ambiguity because it requires reasoning from a certain perspective for the notion of "internal" to make sense. For instance, an asynchronous callback is often though of something "external" from the perspective of the model, yet it would result in internal actions. Sounds pretty confusing. Another reason to prefer action over internal is that (like the other keywords) action is a noun. Nouns are more easily referenced in text than adjectives.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

edwardalee commented 5 years ago

Feel free to put these on the related work wiki page (with comments on how they are related, like the ones already there). That page will be where we keep track...

Edward


Edward A. Lee EECS, UC Berkeley eal@eecs.berkeley.edu http://eecs.berkeley.edu/~eal

On Apr 23, 2019, at 9:23 PM, MarjanSirjani notifications@github.com wrote:

— Timed Input Output Transition System (TIOTS) as semantics of DE

We used TIOTS as semantics of our Coordinated Actor Model in http://rebeca-lang.org/assets/papers/2018/Runtime-Compositional-Verification-of-Self-adaptive-Systems.pdf

The paper is not yet published, we sent it to IEEE TSE last Nov. but it got rejected. I sent an older version to Edward last spring (2018). The paper is not easy to read, and I am trying to break it in two, and give the semantics of Magnifier in TIOTS (see figure 2), and semantics of DE as SOS rules (Section 4). I’ll send you a better version when we have one.

Our semantics is based on two papers on Timed I/O Automata (TIOA) and Timed Input Output Transition System (TIOTS) or timed input-output LTS (TIOLTS) in two papers, one by Kim Larsen and other one by Stavros.

Compositional Verification of Real-Time Systems Using Ecdar Alexandre David and Kim. G. Larsen and Axel Legay and Mikael H. Møller and Ulrik Nyman and Anders P. Ravn and Arne Skou and Andrzej Wąsowski

and Conformance Testing for Real-Time Systems Moez Krichen and Stavros Tripakis

On 23 Apr 2019, at 18:55, Marten Lohstroh notifications@github.com<mailto:notifications@github.com> wrote:

The connection with IO Automata suggests that we could change the keyword “action” to “internal”. Thoughts? Edward

I thought of this option, too, but I realized it introduces ambiguity because it requires reasoning from a certain perspective for the notion of "internal" to make sense. For instance, an asynchronous callback is often though of something "external" from the perspective of the model, yet it would result in internal actions. Sounds pretty confusing. Another reason to prefer action over internal is that (like the other keywords) action is a noun. Nouns are more easily referenced in text than adjectives.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

edwardalee commented 5 years ago

The distinction we are making is between ports and other triggers for reactions. Ports are a central concept in LF because they enable causality analysis, which enables determinism. This concept is missing in Rebecca, Akka, Ray, and many other approaches to actor-based modeling.

All reactions are triggered by events, which occur at a logical time. Some events come in through ports, some from timers (enabling timing analysis), and some from external asynchronous events.

Edward


Edward A. Lee EECS, UC Berkeley eal@eecs.berkeley.edu http://eecs.berkeley.edu/~eal

On Apr 23, 2019, at 9:04 PM, MarjanSirjani notifications@github.com wrote:

— Events and Reactions; and why callbacks/actions are different?

I understand two general concepts for actors: events and reactions In Timed Rebeca we have message servers that are reactions in LF, and react to events (messages), and messages/events that are sent (triggered and will be served by the receiver).

We can have time-triggered events, or events sent by other actors. See http://rebeca-lang.org/assets/papers/2014/Timed-Rebeca-Shift-Equivalency-published.pdf http://rebeca-lang.org/assets/papers/2014/Modelling%20and%20simulation%20of%20asynchronous%20real-time%20systems%20using%20Timed%20Rebeca.pdf

I don’t understand why you are treating call-backs differently. Would you please explain?

On 23 Apr 2019, at 18:55, Marten Lohstroh notifications@github.com<mailto:notifications@github.com> wrote:

The connection with IO Automata suggests that we could change the keyword “action” to “internal”. Thoughts? Edward

I thought of this option, too, but I realized it introduces ambiguity because it requires reasoning from a certain perspective for the notion of "internal" to make sense. For instance, an asynchronous callback is often though of something "external" from the perspective of the model, yet it would result in internal actions. Sounds pretty confusing. Another reason to prefer action over internal is that (like the other keywords) action is a noun. Nouns are more easily referenced in text than adjectives.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20%23issuecomment-485825561&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C8afdc04da2064001718208d6c7f77e22%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636916263128328234&sdata=nJyx2A6P76dQL%2B7ZRUv5NQUqqLHDSdxZFwXgOV8ho28%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYC4R7O5XU4JYSSDKK3PR4L4LANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C8afdc04da2064001718208d6c7f77e22%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636916263128328234&sdata=CW1uufnuzNbkz1%2FSCpfSCqNLhxrfwnL%2FgyejgRfSfII%3D&reserved=0.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

MarjanSirjani commented 5 years ago

Sure. I wrote it here because of the discussion on IO Automata, and you mentioned one of the two main differences being the model of time. There is a timed version of IO Automata, TIOA, which we used.

On 24 Apr 2019, at 18:14, Edward A. Lee notifications@github.com<mailto:notifications@github.com> wrote:

Feel free to put these on the related work wiki page (with comments on how they are related, like the ones already there). That page will be where we keep track...

Edward


Edward A. Lee EECS, UC Berkeley eal@eecs.berkeley.edumailto:eal@eecs.berkeley.edu http://eecs.berkeley.edu/~eal

On Apr 23, 2019, at 9:23 PM, MarjanSirjani notifications@github.com<mailto:notifications@github.com> wrote:

— Timed Input Output Transition System (TIOTS) as semantics of DE

We used TIOTS as semantics of our Coordinated Actor Model in http://rebeca-lang.org/assets/papers/2018/Runtime-Compositional-Verification-of-Self-adaptive-Systems.pdf

The paper is not yet published, we sent it to IEEE TSE last Nov. but it got rejected. I sent an older version to Edward last spring (2018). The paper is not easy to read, and I am trying to break it in two, and give the semantics of Magnifier in TIOTS (see figure 2), and semantics of DE as SOS rules (Section 4). I’ll send you a better version when we have one.

Our semantics is based on two papers on Timed I/O Automata (TIOA) and Timed Input Output Transition System (TIOTS) or timed input-output LTS (TIOLTS) in two papers, one by Kim Larsen and other one by Stavros.

Compositional Verification of Real-Time Systems Using Ecdar Alexandre David and Kim. G. Larsen and Axel Legay and Mikael H. Møller and Ulrik Nyman and Anders P. Ravn and Arne Skou and Andrzej Wąsowski

and Conformance Testing for Real-Time Systems Moez Krichen and Stavros Tripakis

On 23 Apr 2019, at 18:55, Marten Lohstroh notifications@github.com<mailto:notifications@github.commailto:notifications@github.com> wrote:

The connection with IO Automata suggests that we could change the keyword “action” to “internal”. Thoughts? Edward

I thought of this option, too, but I realized it introduces ambiguity because it requires reasoning from a certain perspective for the notion of "internal" to make sense. For instance, an asynchronous callback is often though of something "external" from the perspective of the model, yet it would result in internal actions. Sounds pretty confusing. Another reason to prefer action over internal is that (like the other keywords) action is a noun. Nouns are more easily referenced in text than adjectives.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20%23issuecomment-486235907&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C1be1c4b1d95f48d043db08d6c8bb0625%7Ca1795b64dabd4758b988b309292316cf%7C0%7C1%7C636917102923874985&sdata=LhlLiOXb7PYWMHrf5fb9m%2BDKMK49fp60Zm28C%2BZ0H50%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYFUZPCWMKQ3AZUHIODPSBP5DANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C1be1c4b1d95f48d043db08d6c8bb0625%7Ca1795b64dabd4758b988b309292316cf%7C0%7C1%7C636917102923884990&sdata=wwKyPm1pTG7ZzXmFyUmbyx2FD4XxF9kGp%2BzQXJlrEmo%3D&reserved=0.

MarjanSirjani commented 5 years ago

Thank you for the explanation, I think I understand. Then you may want to be more careful with the naming, as I see both input ports and external asynchronous events as inputs. They are both coming from outside … Maybe I am missing something.

On 24 Apr 2019, at 18:20, Edward A. Lee notifications@github.com<mailto:notifications@github.com> wrote:

The distinction we are making is between ports and other triggers for reactions. Ports are a central concept in LF because they enable causality analysis, which enables determinism. This concept is missing in Rebecca, Akka, Ray, and many other approaches to actor-based modeling.

All reactions are triggered by events, which occur at a logical time. Some events come in through ports, some from timers (enabling timing analysis), and some from external asynchronous events.

Edward


Edward A. Lee EECS, UC Berkeley eal@eecs.berkeley.edumailto:eal@eecs.berkeley.edu http://eecs.berkeley.edu/~eal

On Apr 23, 2019, at 9:04 PM, MarjanSirjani notifications@github.com<mailto:notifications@github.com> wrote:

— Events and Reactions; and why callbacks/actions are different?

I understand two general concepts for actors: events and reactions In Timed Rebeca we have message servers that are reactions in LF, and react to events (messages), and messages/events that are sent (triggered and will be served by the receiver).

We can have time-triggered events, or events sent by other actors. See http://rebeca-lang.org/assets/papers/2014/Timed-Rebeca-Shift-Equivalency-published.pdf http://rebeca-lang.org/assets/papers/2014/Modelling%20and%20simulation%20of%20asynchronous%20real-time%20systems%20using%20Timed%20Rebeca.pdf

I don’t understand why you are treating call-backs differently. Would you please explain?

On 23 Apr 2019, at 18:55, Marten Lohstroh notifications@github.com<mailto:notifications@github.commailto:notifications@github.com> wrote:

The connection with IO Automata suggests that we could change the keyword “action” to “internal”. Thoughts? Edward

I thought of this option, too, but I realized it introduces ambiguity because it requires reasoning from a certain perspective for the notion of "internal" to make sense. For instance, an asynchronous callback is often though of something "external" from the perspective of the model, yet it would result in internal actions. Sounds pretty confusing. Another reason to prefer action over internal is that (like the other keywords) action is a noun. Nouns are more easily referenced in text than adjectives.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20%23issuecomment-485825561&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C8afdc04da2064001718208d6c7f77e22%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636916263128328234&sdata=nJyx2A6P76dQL%2B7ZRUv5NQUqqLHDSdxZFwXgOV8ho28%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYC4R7O5XU4JYSSDKK3PR4L4LANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C8afdc04da2064001718208d6c7f77e22%7Ca1795b64dabd4758b988b309292316cf%7C0%7C0%7C636916263128328234&sdata=CW1uufnuzNbkz1%2FSCpfSCqNLhxrfwnL%2FgyejgRfSfII%3D&reserved=0.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Ficyphy%2Flingua-franca%2Fissues%2F20%23issuecomment-486241105&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C41e413252b5f42128efe08d6c8bbcbfb%7Ca1795b64dabd4758b988b309292316cf%7C0%7C1%7C636917106240474998&sdata=LCILZ0moARNVzcWZUclyIQPTr7tcCJkazXW2mS8uS%2BY%3D&reserved=0, or mute the threadhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAKN3EYCLOKLBA6AOGOAAH3LPSBQR3ANCNFSM4HHAWV4Q&data=02%7C01%7Cmarjan.sirjani%40mdh.se%7C41e413252b5f42128efe08d6c8bbcbfb%7Ca1795b64dabd4758b988b309292316cf%7C0%7C1%7C636917106240485007&sdata=dA9MgH%2Fl%2BbdVNDPP2eVHelwWvYb%2FzUtIFh8VZnCGFhA%3D&reserved=0.

lhstrh commented 5 years ago

We elected the timer keyword to replace the clock keyword. Anyone who feels they have a better alternative for timer, feel welcome to reopen this ticket.