mbeddr/mbeddr.formal

Array access

mfgpcm opened this issue · 1 comments

mfgpcm commented

While it is possible to define arrays, it is not possible to access elements of arrays. Also, the nary AND and nary OR do not work as expected for arrays.
Example:
Legal mbedder.formal SMV:

MODULE main {                                 
  VAR {                                       
    x : array 0..5 of boolean;                
  }                                           
  DEFINE {                                    
    y := [TRUE, TRUE, TRUE, TRUE, TRUE, TRUE];
  }                                           
  LTLSPEC x = y;                              
  LTLSPEC [& x ] = TRUE;                      
}

Generated is the following plain SMV, which leads to a "TYPE ERROR file system.smv: line 7 : illegal operand types of "=" : array 0..5 of boolean and boolean; ERROR: Property "x = TRUE" is not correct or not well typed.":

MODULE main
  VAR
    x : array 0..5 of boolean;
  DEFINE
    y := [TRUE, TRUE, TRUE, TRUE, TRUE, TRUE];
  LTLSPEC x = y
  LTLSPEC x = TRUE

What I would like to have is

  1. to be able to write LTLSPEC x[0] = y[0]; in mbedder.formal being translated to the same in plain SMV (2) and
  2. the [& x ] = TRUE in mbedder.formal to be expanded to (x[0] & x[1] & x[2] & x[3] & x[4] & x[5]) = TRUE in plain SMV.
danielratiu commented

I have implemented the posibility to access array elements like e.g. x[0] = y[0]

Regarding the n-ary AND, its intent is that it takes several arguments (expressions) and joins them with '&'
The intent of this extension is not to work with arrays - actually, due to the weak type-system of SMV, in general, we do NOT know if a variable has array type (e.g. if a formal parameter is referenced)

  • 👍1