Open mforets opened 4 years ago
These are the most obvious preconditions.
Reachability
.SetBasedRecurrences
should be independent of Reachability
. Thus we need to break some dependencies.Here are some examples:
terminate
function that is applied in each iteration (we already have something like this in some places for out-of-invariant checks, but property checking is still implemented differently). (This is not an argument against #678.)RecurrenceAlgorithm
or something such that a concrete algorithm is a subtype of that interface. To specify the concrete algorithm, do Reachability
users create an object of a subtype (as they currently do) or do they specify a String
/Symbol
and Reachability
creates these objects internally? (See also the next item.)Reachability
? Clearly we cannot pass an Options
struct (because of item 2. above). I see the following choices:
AlgoXOptions
structs in SetBasedRecurrences
.
+) Options can be created by the user when creating the algorithm.
-) Options have to be set by the user when creating the algorithm.
-) In Reachability
we may call an algorithm several times in a (hybrid) loop but with different options. So we would need to modify these options, which may break assumptions.AbstractSolution
. The AbstractSolution
type and its subtypes hence need to live in SetBasedRecurrences
to satisfy item 2. above.
Alternatively we can pass a process
function (which would be a generalization of the terminate
function above). Then the algorithm need not return anything and instead this function takes care of storing the set in a vector and/or checking a property/invariant.
Here is an example how this process
function could work:
X = first()
while process(X)
X = post(X)
end
As per offline discussion in JuliaReachDays1, it would be nice to outsource some of the core reachability algorithms to a new package called
SetBasedRecurrences.jl
(which is now empty).Let me open this issue to gather the action points and a discussion thread before actually making the changes. Some pros and cons are collected below (some of the comments in this issue apply here as well).
cc: @dfcaporale
Pros:
Cons:
Reachability.jl
andSetBasedRecurrences.jl
? there will be some overlap..