Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Question about encoding in dreach format #288

Open
elmiraafra opened this issue Dec 26, 2022 · 0 comments
Open

Question about encoding in dreach format #288

elmiraafra opened this issue Dec 26, 2022 · 0 comments

Comments

@elmiraafra
Copy link

elmiraafra commented Dec 26, 2022

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 ;

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant