dmitrydrozdov / fb2smv Goto Github PK

Let us start a proper documentation for FB2SMV

Add support for Adapters

1. Currently instances of E_DELAY need to have different names.
2. For E_DELAY FBs instances FB2SMV inserts, I got it going after deleting the statement
   init(T2_DO):= -1;
   for the E_DELAY instance name T2

VAR T2 : E_DELAY (T2_START, T2_STOP, T2_EO, T2_DT, T2_DI, T2_DO, T2_alpha, T2_beta);
init(T2_START):= FALSE;
init(T2_STOP):= FALSE;
init(T2_EO):= FALSE;
init(T2_DT):= 666;
init(T2_DI):= -1;
init(T2_DO):= -1;
init(T2_alpha):= FALSE;
init(T2_beta):= FALSE;

NuSMV complains about the double assignment of this variable because inside the E_DELAY module there is already such an assignment init(DO_):= -1;

MODULE E_DELAY(event_START, event_STOP, event_EO, DT_, DI_, DO_, alpha, beta)
ASSIGN
init(DO_):= -1;
next(DO_):= case
alpha & event_START : DT_;
alpha & event_STOP : -1;
alpha & DI_ = 0 : -1;
DI_ >= 0 : DI_;
TRUE: DO_; TRUE : DO_;
esac;
DEFINE event_START_reset:= alpha;
DEFINE event_STOP_reset:= (alpha & (event_START));
DEFINE event_EO_set:= (alpha & DI_=0);
DEFINE alpha_reset:= alpha;
DEFINE beta_set:= alpha;
FAIRNESS (alpha)
FAIRNESS (beta)

Besides, FB2SMV defines some variables of E_DELAY as integer

VAR T2_DT :integer;
VAR T2_DI : integer;
VAR T2_DO : integer;

I changed it manually to:
VAR T2_DT : -1..666;
VAR T2_DI : -1..666;
VAR T2_DO : -1..666;

Because I found later initialisation
init(T2_DT):= 666;