Discuss state space generation performance bottleneck

[AndreaPuffo]

Our activity synthesis chain generates the state space at step 4. This can be time-consuming, especially when most variables are unrelated / "don't-cares" for the activity (but are related to other activities). This is particularly annoying given that in steps 6 and 7 we minimize the state space, which again becomes time-consuming with a large state space, and slows down the language equivalence check, which also computes the state space.

Current solution: the user manually specifies the values of all variables in the activity preconditions. This is error-prone and annoying for a user, but gets the job done. Ideally, we would avoid this.

The performance difference can be quite staggering. For instance, the LSAT bowling ball example contains 8 low-level activities (out of a total of 10 activities) that are loosely correlated, i.e. the variables used in one activity practically do not overlap with the ones of another. Synthesizing with "liberal" preconditions the total time is around 1000 seconds, with "strict" preconditions is around 14 seconds.

Possible future directions:

• Before synthesis, automatically detect unrelated variables and give them a value: quick-and-dirty solution, should not be too much work to implement;
• Use a symbolic state space explorer: definitely the way to go, but I believe much more time-consuming.

[wytseoortwijn]

Before synthesis, automatically detect unrelated variables and give them a value: quick-and-dirty solution, should not be too much work to implement;

I'm not so whether this is so easy. It may be tricky to determine which variable is (un)related. We could analyze the occurrence constraints of abstract activities (plus the nodes of any concrete activities that are being called). But if we would ever want to get rid of occurrence constraints, this trick would no longer work.

Before resolving this issue, I think we need to have a serious look first at what would be needed to implement a symbolic state space explorer.