mbeddr / mbeddr.formal

FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.
https://sites.google.com/site/fastenroot/home
Apache License 2.0
23 stars 14 forks source link

Mapping of connections while flattening does not work for structs #34

Closed mfgpcm closed 4 years ago

mfgpcm commented 4 years ago

(Sorry for creating the next issue instead of fixing it and creating a pull request. I know it's a bad excuse but I still couldn't acquire the necessary open source contribution rights.) Here is a minimal example in FASTEN:

struct struct1 {                
  b : boolean;                  
}                               

interface iin                   
  in : struct1 => no output     
contract:                       
  no contract                   
interface iout                  
  no input => out : struct1     
contract:                       
  no contract                   
assembly a                      
  no input => no output         
contract:                       
  no contract                   
  body: iin i1;                 
        iout i2;                
        connect i2.out to i1.in;

This is translated to

MODULE a___flattened
  VAR
    i1_DOT_in : struct1_struct;
    i2_DOT_out : struct1_struct;

  DEFINE
    arch_wiring := (i2_DOT_out = i1_DOT_in);

MODULE main
  VAR
    flattened : a___flattened;

MODULE struct1_struct
  VAR
    b : boolean;

which results in a file a___flattenedSystem.smv: line 7: "flattened.i2_DOT_out" undefined in definition of flattened.arch_wiring at line 12. I think, should be arch_wiring := (i2_DOT_out.b = i1_DOT_in.b);, so the flattening needs to map all individual elements of the struct / the MODULE.