MC gets null ob ject in Formula generation

[pglvdm]

Using a model such as:

channels

  left, left1, left2, mid, right : nat

values 

  a : nat = 2

  b : nat = 5

process DataFlow = begin

actions

  X21 = left1?x -> mid!(a * x) -> X21

  X22 = left2?y -> mid?z -> right!(z + b*y) -> X22

  X23 = left?x -> left1!x -> X24

  X24 = left?x -> left2!x -> left1!x -> X24

@ 

  X23 [| {| left1,left2 |} |]
    ( X21 [| {| mid |} |] X22 )

end

gives an error: "could not analyse the secification. Internal error when accessing some null ob ject during FORMULA script generation"

[adalbertocajueiro]

That is because the model uses expressions in communications. Expressions involving operators are (semantically) accepted by the model checker in assignments. An idea to overcome that is to declara local variables of actions (or state variables) and use them to keep the values of expressions. these variables can be communicated.

Moreover, there was a small fix to be done in the conversion from AST to FORMULA.

An alternative model would be:

channels

  left, left1, left2, mid, right : nat

values 

  a : nat = 2

  b : nat = 5

process DataFlow = 
begin
  state
    zby : nat := 0
actions

  X21 = (dcl ax:nat @ left1?x -> ax := a*x; mid!ax -> X21)

  X22 = left2?y -> mid?z -> zby := z + b*y; right!zby -> X22

  X23 = left?x -> left1!x -> X24

  X24 = left?x -> left2!x -> left1!x -> X24

@ 

  X23 [| {| left1,left2 |} |]
    ( X21 [| {| mid |} |] X22 )

end

process Simple = 
begin
@Skip
end

The above model will be analysed in the next delivery of version 0.3.3.