search

nl-utwente-groove / code

GROOVE code base
https://groove.cs.utwente.nl
5 stars 0 forks source link

Decouple search method from exploration strategy #551

Open rensink opened 12 years ago

rensink commented 12 years ago

Right now the choice of search plan/rete is connected to the choice of exploration strategy. This connection is not natural, the two should be decoupled somehow

Reported by: rensink

rensink commented 12 years ago

Original comment by: rensink

rensink commented 12 years ago

Original comment by: rensink

rensink commented 12 years ago

Serialisation of explorations: - Use unordered set of keywords Esther than fixed list - Categories: search mode (plan, rete, shape), strategy, acceptor, result - Use defaults: DFS, plan, final, infinite

Original comment by: rensink

rensink commented 12 years ago

Original comment by: rensink

rensink commented 12 years ago

Original comment by: rensink

rensink commented 12 years ago

In addition to the search plan, also the choice of algebra should rather be part of the exploration strategy than the grammar properties (as it is now). For instance, STS-based exploration should always use the point algebra.

This means that one of the checks on grammars should also be deferred to the point where the exploration is set, viz. the binding of all data variables.

Original comment by: rensink

rensink commented 11 years ago

Original comment by: zambon

rensink commented 11 years ago

This is a summary of all the previous comments plus some additional information from the current code state.

The idea is that we should be able to construct an Exploration Configuration (EC) that completely gathers all aspects of state space generation. Each aspect should be uniquely identified by a keyword, to allow for the serialization of the EC as a string that can be kept in the grammar properties. I won't try to list/create the keywords now, I guess it's better to leave that to the moment when this ticket is implemented.

The major point of decoupling is between the exploration strategy and the matching method, which should be orthogonal. Current strategies such as 'shapedfs' make no sense. Below I'll list each aspect that I think should compose the EC, along their possible options and some other comments.

- Strategy. The ones that shoud remain are: * DFS. This should be the default strategy, not BFS as is currently the case. * BFS * Linear * Random * Conditional, with three variants: Rule, Node Bound, Edge Bound. These strategies all currently use BFS but I don't really see why. In fact I don't believe these should actually be strategies because they don't really say HOW the state space should be traverse but actually WHEN to stop. It seems we should break down the Acceptors in two categories, one called Result Acceptors that are like the ones we have now, that collect Result states. And a new category called State Acceptor, that actually decide if the state can be part of the state space or not. * Remote. This would connect to the current discussions on using GROOVE as a server.

- Match Method: * For concrete exploration: Search Plan or Rete * For abstraction exploration: Neighbourhood or Pattern Shape Matching. (This requires refactoring of the current 'match' packages laying around.)

- Acceptors: * Final States * Invariant Check * Rule Application * Rule Formula * Any State * No State * Cycle. This should be available only programmatically as it is used in LTL model checking, but currently it is showing in the Generator options.

- Result Count: a Natural number (no change)

- Algebra Family: * Default (Java) * Big * Point * Term

There are, of course, some restrictions on how these parameters can be combined. This conditions will probably arise automatically when this ticket gets to be implemented.

Original comment by: zambon