Outsource reachability algorithms to a new package

[mforets]

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:

• (set based) recurrences are interesting on its own and can live independently from the Reachability API (reachability options layer, ...)
• ideally, it will simplify adding new reachability algorithms
• easier path to get the package registered
• easier (?) to aim at better code coverage and add missing docs if we start from scratch

Cons:

• a new package / git repo to maintain
• how do we handle documentation between Reachability.jl and SetBasedRecurrences.jl? there will be some overlap..

[schillic]

These are the most obvious preconditions.

1. Define the input/output interface to Reachability.
2. SetBasedRecurrences should be independent of Reachability. Thus we need to break some dependencies.

Here are some examples:

• For checking properties during recurrence computation it seems that we need to outsource properties (Outsource Properties to a new package #678) to satisfy item 2. above. However, I would rather prefer to define the interface for item 1. to accept an anonymous 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 Outsource Properties to a new package #678.)
• There will probably be an interface 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.)
• How do we pass options from Reachability? Clearly we cannot pass an Options struct (because of item 2. above). I see the following choices:
  1. Create algorithm-specific 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.
  2. Pass the options as function arguments.
     -) very long function calls
• The result of an algorithm is an 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