Open valvyat opened 3 years ago
Regarding your last comment, if you disable "integers and reals" switch in the settings, it supposed to change all integer types into ranges. And then you can manually edit the ranges ("SMV Type") in the GUI "Variables" tab if you need
Please, share an FB application where you run into these errors
Regarding your last comment, if you disable "integers and reals" switch in the settings, it supposed to change all integer types into ranges. And then you can manually edit the ranges ("SMV Type") in the GUI "Variables" tab if you need
Thanks! Please note that I am using the command line version. Implementing this would require some work by Midhun.
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 EDELAY module there is already such an assignment init(DO):= -1;
MODULE E_DELAY(event_START, event_STOP, eventEO, DT, DI, DO, alpha, beta) ASSIGN init(DO):= -1; next(DO):= case alpha & eventSTART : DT; alpha & eventSTOP : -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_EOset:= (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;