Wrong initial states in flattened model

[ttj]

We have a model of the DC microgrid that Omar has been working on in SpaceEx. He's able to analyze the original (networked) model in SpaceEx. However, when flattening with Hyst (so we can then use the SLSF translator), the initial states do not seem to get created correctly, in particular, they retain their old names instead of being converted to the new variable names. An example of the input and output models are attached, as well as a screenshot of the networked model.

This is probably related to some of the discussion Stan and I had on initial states, but wanted to raise it as a possible issue. I also noticed the simplification engine left around a variety of redundant expressions (e.g., control_i = 1 and control_i = 1). We both used Windows, but I'll try it on Linux as well to see if the python interfaces do better.

dc_microgrid.zip

[stanleybak]

Could you clarify your statement that:

[the variables] retain their old names instead of being converted to the new variable names

What do you mean by the old names and new names? Are the old names the parent names, and the new names the names in the child automaton? Or vice-versa? I believe the parent names should always be used when flattening (since what if a there are two children which use the variable, with different child names?).

Could you create a minimal example that demonstrates the error? For example, can a single-variable networked automaton, with simple timer dynamics have the same issue?

[stanleybak]

In terms of the simplification engine, the built-in one only simplifies expressions of the form (CONSTANT [OP] CONSTANT), so it makes sense that it would miss this one. We probably want to (eventually) write a model optimization pass that could pass these to an SMT solver to check for such redundancy.

[ttj]

Omar: please clarify and add a small example that has this issue if
possible.

http://www.taylortjohnson.com/

On Wed, Feb 24, 2016 at 12:41 PM, Stanley Bak notifications@github.com
wrote:

Could you clarify your statement that:

[the variables] retain their old names instead of being converted to the
new variable names
What do you mean by the old names and new names? Are the old names the
parent names, and the new names the names in the child automaton? Or
vice-versa? I believe the parent names should always be used when
flattening (since what if a there are two children which use the variable,
with different child names?).

Could you create a minimal example that demonstrates the error? For
example, can a single-variable networked automaton, with simple timer
dynamics have the same issue?

—
Reply to this email directly or view it on GitHub
#26 (comment).

[omarali75]

Sorry to respond you late. The input to hsyt is the network model for dc microgrid, that contains two converters each controlled by its corresponding controller.

hyst generates the flattened model with new variables and constants. Moreover, the initial values for newly created variables as well as the constants are not defined in the cfg file created by hyst during flattening.

[stanleybak]

Hmm, that does sound incorrect. Could you create a minimal example that demonstrates the issues (1 variable, 1-2 child automata, perhaps)?

[omarali75]

Sure, I'll be working on it and forward it to you in due course.

[omarali75]

I have a simple example that shows the same behavior mentioned above. The automata are sharing information within the network, such that their executions are dependent upon this shared information.
So in this example, we have two plants 'i' and 'j' (1 variable each), each plant controlled by its corresponding controller (1 variables each), with global time 'gt' defined for the entire network. The controllers share information with each other, through shared variables x_pu.
Please use simpler_spaceex.cfg in the attached zip file for SpaceEx analysis if required.
example.zip

[stanleybak]

thanks omar. One more thing. What is the observed problem when this model is converted (specifically) and what is the expected behavior?

[omarali75]

Hyst generates new variables and constants after conversion, in addition to existing ones defined in the original model. These new variables and constants are named based on the locations within the network. The problem observed is: neither these variables are initialized nor new constants are defined in the generated cfg file. So the expected behavior is that the generated cfg file should have the new variables initialized and new constants defined.
An observation linked to above is that, the conversion process increases the complexity of the model by generating more variables and constants.

[stanleybak]

I looked at the example and I can't easily see what the problem is. Can you make it as simple as possible? For example, currently it's a network automaton with 5 child automata. Does showing the problem require 5 children? If not, delete them until there is only one or two children. Each of the automata has two modes. Is this necessary? If one mode is enough to show the problem, make them one-mode automata. The simpler automaton you attached has 7 variables, 2 labels, and 3 constants. Are all of these necessary? Make it a one-variable automaton, or one variable and one label (if that's needed) and it becomes significantly simpler to debug. In the init you have "i_Li==1.6". Change this to be 0, unless the 1.6 part is critical to show the problem.

Second, please be more specific when stating the problem:

neither these variables are initialized nor new constants are defined in the generated cfg file. So the expected behavior is that the generated cfg file should have the new variables initialized and new constants defined.

For example, say variable instance1.x is renamed to new_x in the flat automata, but in the initial states in the converted model still refer to instance1.x, whereas it is expected that it should also be renamed to new_x

[omarali75]

I have been working to generate some simpler examples exhibiting the same behavior in light of the questions that you had raised. I have attached two examples (i.e. 'example.xml' and 'example2.xml' and related cfg files) that are comparatively simpler than the one I sent you earlier but these do not exhibit the behavior under discussion. For the attached model files, hyst does not generate new variables, rather uses the same variables as that of the model prior conversion, e.g, x, i, gt. It does generate new constants, and discards the constants of the model being converted. But the problem of redundant invariants is there, i.e., hyst generates redundant invariants, e.g, "control == 1 & control == 1" for these simpler examples. Whereas, it is expected that only one such invariant is generated, i.e., "control == 1". The converted models when analyzed in SpaceEx resulted in runtime error related to

So above in view, I thought that the problem requires more automatons. Accordingly, I modified the model, and retained the same number of children automatons, but reduced the number of variables and constants in 'simpler.xml'. As I used hyst to convert the model, it did not generate any new variable in the transformed model, however, it did generate new constants (i.e., 'clock_1_tmax', 'converteri_1_V_ini', and 'converterj_1_V_inj'. It also retained the corresponding constants from the model being converted (i.e., 'tmax', 'V_ini', and 'V_inj'). As above, when anlyzed in SpaceEx, the flatten model produced following runtime error:
ERROR: Error computing time elapse in component , location loc(simpler)==clock1_close_i_close_j_close_i_close_j
caused by: finite_symmetric_bounding_box not allowed with unbounded set:
unbounded in direction [simpler_net.gt=-0,simpler_net.i_Li=-1,simpler_net.x_pui=-0,simpler_net.x_puj=-0,simpler_net.control_i=-0,simpler_net.i_Lj=-0,simpler_net.control_j=-0,simpler_net.clock_1_tmax=-0,simpler_net.converteri_1_V_ini=-1,simpler_net.converterj_1_V_inj=-0,simpler_net.tmax=-0,simpler_net.V_ini=-0,simpler_net.V_inj=-0]
in set: simpler_net.i_Li == 0 & simpler_net.x_pui == 0 & simpler_net.gt == 0 & simpler_net.x_puj == 0 & simpler_net.i_Lj == 0 & simpler_net.control_i == 1 & simpler_net.control_j == 1 & simpler_net.tmax == 0.07 & simpler_net.V_ini == 70 & simpler_net.V_inj == 70 & simpler_net.gt >= 0 & simpler_net.gt-simpler_net.clock_1_tmax <= 0 & simpler_net.control_i == 1 & simpler_net.control_j == 1 & simpler_net.control_i == 1 & simpler_net.control_j == 1
There were runtime errors. Terminating execution.

I have also tried to reduce the modes of the automata. So in example3.xml, I have reduced the modes for both the converters (from two modes to one mode). I successfully analyzed it in SpaceEx. But during hyst conversion, it failed the invariant pass as per following error message in hyst:
"Automaton Export Exception while exporting: Hybrid Automaton IR structure was corrupted after running pass com.verivital.hyst.passes.basic.RemoveSimpleUnsatInvariantsPass".

To summarize above, the file 'simple.xml' truly depicts the problem of generating new variables and new constants altogether. I have attached all the files here.

examples.zip

[stanleybak]

The issue with the first two (example and example2), redundant invariants, is caused by "controli == 1" as a state invariant in two different automata. When they are merged, the invariants are combined. This shouldn't affect reachability though. I would submit this as a separate issue, as an enhancement. I'm not sure why spaceeex has a runtime error on these (what was the errror? I think half of the last sentence was missing)

For the simpler.xml, It's creating new constants for 'clock_1_tmax' because in the network automaton, tmax is NOT connected to clock_1's tmax port. the tmax port instead is mapped to the constant 0.07. Thus, there are two variables here, the global t_max and clock_1's tmax, which is why a new constant clock_1_tmax is created. I guess this is also what's going on with V_inj and V_ini (let me know if this is wrong). Again, I'm not sure why SpaceEx produces an error on this model. It seems the created model is correct. What is wrong with the model being created?

The failing RemoveSimpleUnsatInvariantsPass pass is a third possible problem. This seems like a problem with Hyst. Please create a separate issue for this one as well, with the example3.xml file.

[omarali75]

1a. The run-time error generated during SpaceEx analysis is same as that for simpler.xml. The error for example_flat.xml (hyst conversion of example.xml) is:
"ERROR: Error computing time elapse in component , location loc(example)==close_close
caused by: finite_symmetric_bounding_box not allowed with unbounded set:
unbounded in direction [example_net.i=-1,example_net.x=-0,example_net.control=-0,example_net.converter_V=-1]
in set: example_net.i == 0 & example_net.x == 0 & example_net.control == 1 & example_net.control == 1 & example_net.control == 1
There were runtime errors. Terminating execution."

1b. Whereas, that for example2_flat.xml (hyst conversion of example2.xml) is similar:
"ERROR: Error computing time elapse in component , location loc(example2)==clock1_close_close
caused by: finite_symmetric_bounding_box not allowed with unbounded set:
unbounded in direction [example2_net.gt=-0,example2_net.i=-1,example2_net.x=-0,example2_net.control=-0,example2_net.clock_1_tmax=-0,example2_net.converter_V=-1]
in set: example2_net.i == 0 & example2_net.x == 0 & example2_net.control == 1 & example2_net.gt >= 0 & example2_net.gt-example2_net.clock_1_tmax <= 0 & example2_net.control == 1 & example2_net.control == 1
There were runtime errors. Terminating execution."

1. So for simpler_flat.xml (i.e., the hst conversion of simpler.xml), the error is same as above. I am not sure that exactly where the problem is with the converted model file.
   Since the error being generated is similar to 1a and 1b above, so I'll try to first figure it out for 1a.

For 'simpler.xml', I have linked the constants tmax, V_ini, and V_inj (in simpler_amend.xml), but the Spaceex generated following error with this modification (under STC scenario):

"ERROR: Error computing time elapse in component , location loc(controli_1)==close_i & loc(controlj_1)==close_j & loc(converteri_1)==close_i & loc(converterj_1)==close_j
caused by: restricting flowpipe to empty domain, don't know what to do
There were runtime errors. Terminating execution."

But SpaceEx does generate the results without any error under LGG scenario. Whereas, if I define these values as constants in xml file (as in simpler.xml), SpaceEx under STC scenario generates the results without any error.

However, during hyst conversion, the issue of generating extra constants is resolved.

1. I have created a new issue for failing RemoveSimpleUnsatInvariantsPass pass and attached example3.xml there.

2. With regards to 'simple.xml', hyst generates following new variables (discarding the corresponding variables from the original xml file);

   a). controli_1_x_mci
   b). controli_1_ti
   c). controlj_1_x_mcj
   d). controlj_1_tj

But these variables are not initialized in the cfg file generated by hyst.

It is pertinent to mention that if I define the constants by linking these to cfg file, I get following error during SpaceEx analysis:

"ERROR: Failed to adapt automaton sys1 to scenario stc.
caused by: Failure inside automaton network sys1.
caused by: Failure in automaton controli_1.
caused by: Failed to adapt guard of transition from location close_i to open_i with label jump_i (id 1).
caused by: The expression is not a conjunction of linear constraints.
caused by: The following is not a linear constraint:
0.2*sys1.controli_1.x_mci - sys1.controli_1.ti/sys1.Ti == 0
caused by: Result of division not a linear expression: (sys1.controli_1.ti) / (sys1.Ti)
There were runtime errors. Terminating execution."

And if I remove Ti and Tf from the transition guards as mentioned in above error, then I get following error in SpaceEx:
"ERROR: Failed to adapt automaton sys1 to scenario stc.
caused by: Failure inside automaton network sys1.
caused by: Failure in automaton converteri_1.
caused by: Failed to adapt flow of location close_i.
caused by: The following are not affine dynamics:
i_Li' == 1/Li_(-1_(rsi + rLi)*i_Li + V_ini) & Ti' == 0 & V_refi' == 0 & Ri' == 0 & Li' == 0 & Ci' == 0 & rsi' == 0 & rLi' == 0 & V_ini' == 0
There were runtime errors. Terminating execution."

So it appears that SpaceEx does not accept the constants to be defined by linking these to cfg file for this model (i.e. simple.xml).

[stanleybak]

If this is the case ('SpaceEx does not accept the constants to be defined by linking these to cfg file'), can you create a simple model with a single constant defined in the cfg file and nothing else to demonstrate the error? The model you're using is still quite complicated.

Is this an issue of constants not being substituted for their values? If so, you can run substitute constants pass to do this.

I'm not really following the problem you're reporting. It seems SpaceEx is sometimes reporting errors, but I'm unclear as to what is wrong with Hyst's output. Could this an issue with SpaceEx? Does the converted model run (and produce the correct result) in Flow*, for example?