dreal/dreal4

Question about encoding in dreach format

Opened this issue · 0 comments

Hey, I want to encode a piece of code with dreach format. I have a 2 time step and in every time step the input of the data would be different. After running every step, it would increase and check the target.I defined the first step in initial section. need to keep for variables the last value ( with prime )

My question is that I think I could not encode, like the following code in dreach while the equations are discrete-time objects and I think they should not encode in the flow d/dt (differential equation).
I do not know where should I exactly define my "equations" and "step+1"**

{ mode 1;

invt:
(step < 2);

flow:
d/dt[n_1_0_it]=(1/ (1 + exp(-1*((n_i_0' * (7026)) + (n_i_1' * (9702)) + (n_i_2' * (6002)) )));
d/dt[n_1_0_ft]= (1/(1 + exp(-1*((n_i_0' * (1170)) + (n_i_1' * (12140)) + (n_i_2' * (2545)) ))) );
d/dt[n_1_0_ct]=( 1/(1 + exp(-1*((n_i_0' * (66181)) + (n_i_1' * (4457)) + (n_i_2' * (-1613)) ))) );
d/dt[n_1_0_Ct_0]=n_1_0_ft' * n_1_0_Ct_0 + n_1_0_it' * n_1_0_ct';
d/dt[n_1_0_ot]= (1/(1 + exp(-1*((n_i_0' * (33624)) + (n_i_1' * (80221)) + (n_i_2' * (103444)) ) ))));
d/dt[n_1_0_v0]= (1/(1 + exp(-1*(n_1_0_Ct_0'))) );
d/dt[n_1_0]= n_1_0_ot' * n_1_0_v0';
d/dt[n_o_0] = (1/ (1 + exp(-1*((n_1_0' * (2758)) + (-1268)))));
d/dt[step]=(step' + 1);

jump:
(step = 1) ==> @1(and (n_i_0' = 0)(n_i_1' = 14928405)(n_i_2' = 33554432)(n_i_3' = 16686701));
}

init:
@1 (and (n_i_0' = 33554432)(n_i_1' = (8834793))(n_i_2' = 0)(n_i_3' = 4322285)));

goal:
@1 (and (n_o_0 < 0.25));

TARGET
step = 2;
n_o_0 > 0.25 ;