The current translation from OS2 specifications to ASP constraints (via the symbolic automaton) handles constraint ranges in a way that limits the diversity of the generated plans.
Current behavior
The ASP encoding directly checks whether each constraint from the OS2 spec holds. This works well when constraints are equalities.
However, for constraints involving ranges, e.g., requiring a distance d between two vehicles to lie in [5, 10], the ASP encoding uses a condition such as:
5 <= d <= 10
In practice, this leads to low diversity in the ASP models:
- The solver tends to pick values that satisfy the range as quickly as possible (often at the boundary).
- The actual value of d is effectively determined by the discretized physics + minimization of the number of steps, not by intentional variation.
- As a result, multiple solver runs produce nearly identical solutions.
Proposed improvement
Instead of leaving ranges unconstrained, we should sample a concrete target value X from the range in the OS2 specification before generating the ASP instance.
For the example above:
- Sample a value X uniformly from [5,10].
- Encode the constraint in ASP as an equality: d = X
- Run clingo with this target.
By repeating this sampling process, we obtain distinct ASP instances and therefore much more diverse plans, as each run attempts to satisfy a different concrete target value.
Implementation sketch
- Perform sampling in the Python script (before invoking clingo).
- Pass the sampled value(s) as parameters to the ASP base program, e.g.: #program base(x).
- Restart clingo from scratch for each new sample.
Duration sampling
The same sampling strategy must be applied to durations from OS2 specifications:
- Sample a target duration T from the specified OS2 duration range.
- Use T to determine the length of the plan (number of time steps).
- Note that:
- Some sampled durations will be infeasible => clingo should simply return UNSAT.
- Sometimes clingo reaches all goals before time T. In this case, the solver must continue producing compliant steps after the goals are first satisfied, maintaining all safety and automaton constraints.
This requires extending the ASP encoding so that, after the goal satisfaction, additional steps continue to satisfy all invariants and constraints until time T.
The current translation from OS2 specifications to ASP constraints (via the symbolic automaton) handles constraint ranges in a way that limits the diversity of the generated plans.
Current behavior
The ASP encoding directly checks whether each constraint from the OS2 spec holds. This works well when constraints are equalities.
However, for constraints involving ranges, e.g., requiring a distance d between two vehicles to lie in [5, 10], the ASP encoding uses a condition such as:
5 <= d <= 10
In practice, this leads to low diversity in the ASP models:
Proposed improvement
Instead of leaving ranges unconstrained, we should sample a concrete target value X from the range in the OS2 specification before generating the ASP instance.
For the example above:
By repeating this sampling process, we obtain distinct ASP instances and therefore much more diverse plans, as each run attempts to satisfy a different concrete target value.
Implementation sketch
Duration sampling
The same sampling strategy must be applied to durations from OS2 specifications:
- Some sampled durations will be infeasible => clingo should simply return UNSAT.
- Sometimes clingo reaches all goals before time T. In this case, the solver must continue producing compliant steps after the goals are first satisfied, maintaining all safety and automaton constraints.
This requires extending the ASP encoding so that, after the goal satisfaction, additional steps continue to satisfy all invariants and constraints until time T.