lenaRB / crml-compiler

Implementation of the CRML to Modelica compiler supported by the ITEA3 EMBRACE project.
6 stars 7 forks source link

fix code generated for CRML models implying external variables to better structure bindings definition and building of verication models #87

Open audrey-jardin opened 1 month ago

audrey-jardin commented 1 month ago

Let's illustrate the problem with the BecomesFalse unit test.

Translating the CRML model:

model BecomesFalse is {
    // Operators on events
    // Events generated when a Boolean becomes false
    Operator [ Clock ] Boolean b 'becomes false' = new Clock (not b);

    // Example of function call
    Boolean b1 is external;
    Clock c_b1_becomes_false is b1 'becomes false';
};

Currently produces the Modelica code below:

model BecomesFalse
model 'becomes false'
output CRMLtoModelica.Types.CRMLClock out;
input CRMLtoModelica.Types.Boolean4 b;
CRMLtoModelica.Types.CRMLClock c0(b=CRMLtoModelica.Functions.not4( b));
CRMLtoModelica.Types.CRMLClock_build c0_init(clock= c0);

equation 
 out =c0;
end 'becomes false';
CRMLtoModelica.Types.Boolean4 b1;
CRMLtoModelica.Types.CRMLClock c_b1_becomes_false = 'becomes false1'.out;
'becomes false' 'becomes false1'(b=b1);
end BecomesFalse;

The problem with such model is that:

  1. Its checking fails since it is locally unbalanced
  2. It is not well prepared for building its corresponding verification model and more specifically to bind the external variables coming from other models.

Option1: Declare the generated model as partial

Pros: No more failing at the checking phase Cons: Difficulties to identify errors during the development phase

Option2: Translate external variables as inputs

model BecomesFalse
model 'becomes false'
output CRMLtoModelica.Types.CRMLClock out;
**input** CRMLtoModelica.Types.Boolean4 b;
CRMLtoModelica.Types.CRMLClock c0(b=CRMLtoModelica.Functions.not4( b));
CRMLtoModelica.Types.CRMLClock_build c0_init(clock= c0);

equation 
 out =c0;
end 'becomes false';
**input** CRMLtoModelica.Types.Boolean4 b1;
CRMLtoModelica.Types.CRMLClock c_b1_becomes_false = 'becomes false1'.out;
'becomes false' 'becomes false1'(b=b1);
end BecomesFalse;

Pros: The model is now locally balanced Cons: Generation of the verification model could be complicated since the bindings definition to connect external variables to the ones provided by another Modelica model could implied more complex expressions than the one authorized in classical Modelica binding equations. For instance, the verification model could be something like:

model BecomesFalse_verif
  extends BecomesFalse(b1=externals.b1);
  CRML_test.ETL.BecomesFalse.BecomesFalse_externals externals
equation 
end BecomesFalse_verif;

This model is working as long as there is no complicated conversions to be done on the outputs of externals model.

Option3: Translate external variables as classical typed variables (with no input prefix)

model BecomesFalse
model 'becomes false'
output CRMLtoModelica.Types.CRMLClock out;
**CRMLtoModelica.Types.Boolean4 b;**
CRMLtoModelica.Types.CRMLClock c0(b=CRMLtoModelica.Functions.not4( b));
CRMLtoModelica.Types.CRMLClock_build c0_init(clock= c0);

equation 
 out =c0;
end 'becomes false';
**CRMLtoModelica.Types.Boolean4 b1;**
CRMLtoModelica.Types.CRMLClock c_b1_becomes_false = 'becomes false1'.out;
'becomes false' 'becomes false1'(b=b1);
end BecomesFalse;

The verification model can then be something like:

model BecomesFalse_verif
  extends BecomesFalse;
  CRML_test.ETL.BecomesFalse.BecomesFalse_externals externals
equation 
  b1=externals.b1;
end BecomesFalse_verif;

Pros: Complicated bindings could be defined with a priori no restriction. Cons: The model is still not locally balanced

@lenaRB @adrpo : I have a preference for option3, but what do you think?