UoY-RoboStar / robosim-textual

This repository contains the plugins for the RoboSim textual editor.
Eclipse Public License 2.0
0 stars 0 forks source link

Clarification required wrt. semantics of SimRefExp #7

Open pefribeiro opened 4 years ago

pefribeiro commented 4 years ago

The syntax for a SimRefExp is fairly complex:

    {SimRefExp} '$' element=[NamedElement|QualifiedName] (
        => '.' exp=Atomic | 
        ('?' variable=[Variable|QualifiedName] (':' predicate=Atomic)?)
    )? 

I have not been able to find a definition of its semantics. I wonder if @madielfilho could provide some details about this. I have a preliminary implementation, but I can only guess at the semantics of this, so I'd like to confirm my understanding is correct and to document it in writing.

madielfilho commented 4 years ago

In RoboSim, SimRefExp defines an input communication. Perhaps, it would be better to change the name of this rule.

pefribeiro commented 4 years ago

Thanks @madielfilho. It is still the case that there is no rule in the semantics for such an expression, so this needs to be defined? For example, how are the attributes exp, variable and predicate used? For a condition on a transition, I assume it's similar to what happens in RoboChart, in a way, but it isn't defined in the manual as far as I can see.

Another issue is, such an expression can be used anywhere, at the moment, and not only in the condition of a transition. So what is the meaning if we write if $In?d then A else B end for example? There is no assignment built into the if statement semantics, so I think this needs to be defined, or, at the very least, disallowed.

pefribeiro commented 4 years ago

Following a discussion with Ana it has been decided that such expressions should not be used anywhere else other than in the conditions of a transition, or in a SendEvent.

In the case of a condition such as $e?v \/ $e_2?v_2 the behaviour is that both variables v and v_2 get the respective value communicated via events e and e_2.

In the case of a condition such as $e?v \/ $e_2?v, then the variable v can be assigned both values (not clear if non-deterministically or not).

I need to check how this impacts the memory model, however.

pefribeiro commented 4 years ago

As an Expression, this has been implemented as:

        if (event instanceof Event) {
            // Case where: $event.exp
            if (e.exp !== null) {
                '''«gu.eventId(event)»==(true.«compileExpression(e.exp, ctx)»)'''
            } else if (e.variable !== null) {
                // TODO: Is this correct? There is no rule in the manual for this kind of expression.
                if (e.predicate !== null)
                '''member(«gu.eventId(event)»,{true.«e.variable.name» | «e.variable.name» <- «compileExpression(e.predicate,ctx)», member(«e.variable.name»,«tg.inplace_type(e.variable.type)»)})'''
                else
                '''member(«gu.eventId(event)»,{true.«e.variable.name» | «e.variable.name» <- «tg.inplace_type(e.variable.type)»})'''
            } else {
                '''member(«gu.eventId(event)»,{true«IF event.type!==null».x__ | x__ <- «tg.inplace_type(event.type)»«ENDIF»})'''
            }
        }

I think this needs to be defined in the RoboSim manual.