Repository navigation
Conversation
a flag can be set to recover initial effects that may have been filtered out by the main encoding, due to being proven unable to support any condition. if set, these the transition store will include transitions corresponding to these ground initial effects, with their default value, which may not necessarily be the one that the original filtered-out effect may have had! (note, however, that this is not impactful for our use case)
…erms on a grounding of its source
… transitions a flag can be set to allow condition transitions to be considered as possible supporters
arbimo
left a comment
There was a problem hiding this comment.
I am not sure this should be merged as a module independent of the lprelax work.
It seems designed to very tightly accomodate the needs of lprelax, and is probably not useful outside of it.
Independtly of that, the module currently lack high-level documentation: what it does ? why ? and how ?
In my understanding, identifying transitions is just a matter of pairing one condition with an effect that share the same source, presence, state variable and end/start timepoint.
This is already not stated clearly.
I am not sure anything beyond that is useful to have as a generally accessible analysis.
One reason for this is that, it seems to me that the non-simple terms are dropped for at least part of the analysis which is probably incorrect outside lprelax. I am also not convinced that the recovering of the closed world assumption effects is worth the complexity it induces.
This PR adds an
analysis::transitionsmodule toaries-timelines.A transition is defined as either a condition, effect, or a pair (condition, effect) where the condition and effect share their source (container action), presence literal, and state variable.
The module notably allows:
SchedEncoder), over "unambiguous" state functions (seenonsimple::collect_nonsimple_conditions_and_effects_to_relax).