Schedule generation works only if launched twice / SMT solution transformation returns invalid set types
Current status
When testing #3801, I’ve noticed that the schedule generation only works when launching the synthesis for a second time. It fails with the following error:
!ENTRY org.fortiss.af3.exploration 4 4 2019-08-23 10:09:03.958
!MESSAGE Error executing DSE:
assertion failed: .
!STACK 0
org.eclipse.core.runtime.AssertionFailedException: assertion failed:
at org.eclipse.core.runtime.Assert.isTrue(Assert.java:113)
at org.eclipse.core.runtime.Assert.isTrue(Assert.java:99)
at org.fortiss.af3.exploration.smt.modeltransformation.SolverRun.updateExplorationSolutionState(SolverRun.java:431)
at org.fortiss.af3.exploration.smt.modeltransformation.SolverRun.solveOptimized(SolverRun.java:402)
at org.fortiss.af3.exploration.smt.modeltransformation.SolverRun.solve(SolverRun.java:201)
at org.fortiss.af3.exploration.smt.backend.Z3Backend.executeDSE(Z3Backend.java:130)
at org.fortiss.af3.exploration.service.internal.DSEBackendService$1.run(DSEBackendService.java:174)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-08-23 10:09:03.959
!MESSAGE org.eclipse.core.runtime.Assert.isTrue(Assert.java:113)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-08-23 10:09:03.960
!MESSAGE org.eclipse.core.runtime.Assert.isTrue(Assert.java:99)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-08-23 10:09:03.960
!MESSAGE org.fortiss.af3.exploration.smt.modeltransformation.SolverRun.updateExplorationSolutionState(SolverRun.java:431)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-08-23 10:09:03.961
!MESSAGE org.fortiss.af3.exploration.smt.modeltransformation.SolverRun.solveOptimized(SolverRun.java:402)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-08-23 10:09:03.961
!MESSAGE org.fortiss.af3.exploration.smt.modeltransformation.SolverRun.solve(SolverRun.java:201)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-08-23 10:09:03.962
!MESSAGE org.fortiss.af3.exploration.smt.backend.Z3Backend.executeDSE(Z3Backend.java:130)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-08-23 10:09:03.962
!MESSAGE org.fortiss.af3.exploration.service.internal.DSEBackendService$1.run(DSEBackendService.java:174)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-08-23 10:09:03.963
!MESSAGE org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Dissection
The error arises when adding a transformed resource schedule in L289 of
the SolverRun class it is returned with the SuperSet type “Route” that
is obviously wrong. This may cause the put operation to fail later.
Moreover, debugging reveals that an IllegalStateException is thrown that
might indicate some invalid write accesses to model elements.
Approach
- Fixup the SuperSet type declaration.
- Investigate & Fix the invalid model access if needed.
- Modify the catch clause in L291 of the SolverRun class to catch all Exceptions to record them. Otherwise, they are silently swallowed.
- Validate containments (export solution to AF3 project & save).
(from redmine: issue id 3804, created on 2019-08-23, closed on 2019-08-26)
- Uploads: