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

Preprocess HS to get only necessary variables #397

Closed
kpotomkin opened this issue Nov 28, 2018 · 4 comments
Closed

Preprocess HS to get only necessary variables #397

kpotomkin opened this issue Nov 28, 2018 · 4 comments
Assignees

Comments

@kpotomkin
Copy link
Collaborator

We want to operate only with variables, which are used in guard and invariant constraints.

For discussion:
Do we need to add variables, the value of which in LinearTransformation is not 1?

@mforets
Copy link
Member

mforets commented Nov 28, 2018

I think that after we detect non-zero coordinates in invariants or guards, as a pre-processing step (the leading coefficient is different from zero), we can choose the continuous time post operator to work with the partition given by the variables that correspond to those coordinates. Does that go in the direction of your question?

@kpotomkin
Copy link
Collaborator Author

@mforets no, I mean if we have ResetMap in the transition, which is not a IdentityMap, should we process it too?

@schillic
Copy link
Member

If we want to support #269, this is a different story, but for the "pure" #275, we do not have to consider assignments (because they are applied after the jump).

Let me add that we actually want to detect these "necessary" variables per location, not globally. In practice that may often be the same, but the idea is more general.
So for each location we want to scan the invariant and all outgoing transitions.

@mforets
Copy link
Member

mforets commented Jan 22, 2019

So for each location we want to scan the invariant and all outgoing transitions.

Note: the output of the initial implementation (in #398) does not distinguish if the variables come from the invariant or from transitions.

schillic added a commit that referenced this issue Jan 22, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants