Z3 based Deployment Synthesis is broken
Observed behavior.
The Z3 backend, or more specific: its Z3 Transformation, produces Exceptions when launching the generation. Two different kinds of exceptions have been observed.
1. Using basic deployment constraints only:
!ENTRY org.fortiss.af3.exploration 4 4 2018-03-29 19:00:03.079
!MESSAGE Error executing DSE:
null.
!STACK 0
java.lang.NullPointerException
at com.microsoft.z3.Context.checkContextMatch(Context.java:4043)
at com.microsoft.z3.Context.checkContextMatch(Context.java:4064)
at com.microsoft.z3.FuncDecl.apply(FuncDecl.java:370)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.createFunctionExpression(ConstraintToNONQuantifiedSMT.java:330)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:127)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBoolean(ConstraintToNONQuantifiedSMT.java:212)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:129)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBinder(ConstraintToNONQuantifiedSMT.java:170)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:125)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBinder(ConstraintToNONQuantifiedSMT.java:170)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:125)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.transfrom(ConstraintToNONQuantifiedSMT.java:112)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.DSMLtoSMTTransformator.extractSMTExpr(DSMLtoSMTTransformator.java:318)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.DSMLtoSMTTransformator.transform(DSMLtoSMTTransformator.java:178)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.SolverRun2.solveOptimized(SolverRun2.java:119)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.DeploymentRun2.solveDeployment(DeploymentRun2.java:98)
at
org.fortiss.af3.exploration.smt.backend.Z3Backend.executeDSE(Z3Backend.java:58)
at
org.fortiss.af3.exploration.backend.DseBackendHandler$1.run(DseBackendHandler.java:167)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:53)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.080
!MESSAGE com.microsoft.z3.Context.checkContextMatch(Context.java:4043)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.080
!MESSAGE com.microsoft.z3.Context.checkContextMatch(Context.java:4064)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.080
!MESSAGE com.microsoft.z3.FuncDecl.apply(FuncDecl.java:370)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.080
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.createFunctionExpression(ConstraintToNONQuantifiedSMT.java:330)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.081
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:127)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.081
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBoolean(ConstraintToNONQuantifiedSMT.java:212)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.081
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:129)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.081
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBinder(ConstraintToNONQuantifiedSMT.java:170)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.081
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:125)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.081
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBinder(ConstraintToNONQuantifiedSMT.java:170)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.081
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:125)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.081
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.transfrom(ConstraintToNONQuantifiedSMT.java:112)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.082
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.DSMLtoSMTTransformator.extractSMTExpr(DSMLtoSMTTransformator.java:318)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.082
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.DSMLtoSMTTransformator.transform(DSMLtoSMTTransformator.java:178)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.082
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.SolverRun2.solveOptimized(SolverRun2.java:119)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.082
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.DeploymentRun2.solveDeployment(DeploymentRun2.java:98)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.082
!MESSAGE
org.fortiss.af3.exploration.smt.backend.Z3Backend.executeDSE(Z3Backend.java:58)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.083
!MESSAGE
org.fortiss.af3.exploration.backend.DseBackendHandler$1.run(DseBackendHandler.java:167)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:00:03.083
!MESSAGE org.eclipse.core.internal.jobs.Worker.run(Worker.java:53)
2. Using a single Objective without basic deployment constraints:
!ENTRY org.fortiss.af3.exploration 4 4 2018-03-29 19:01:08.947
!MESSAGE Error executing DSE:
null.
!STACK 0
java.lang.NullPointerException
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.DSMLTransformationService.getFunctionForLeftSideType(DSMLTransformationService.java:342)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.DSMLTransformationService.getAllocFunctionForLeftSideType(DSMLTransformationService.java:352)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.createAllocationExpression(ConstraintToNONQuantifiedSMT.java:316)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBoolean(ConstraintToNONQuantifiedSMT.java:204)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:129)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBinder(ConstraintToNONQuantifiedSMT.java:170)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:125)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBinder(ConstraintToNONQuantifiedSMT.java:165)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:125)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.transfrom(ConstraintToNONQuantifiedSMT.java:118)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.DSMLtoSMTTransformator.transform(DSMLtoSMTTransformator.java:203)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.SolverRun2.solveOptimized(SolverRun2.java:119)
at
org.fortiss.af3.exploration.smt.modeltransformation.rework.DeploymentRun2.solveDeployment(DeploymentRun2.java:98)
at
org.fortiss.af3.exploration.smt.backend.Z3Backend.executeDSE(Z3Backend.java:58)
at
org.fortiss.af3.exploration.backend.DseBackendHandler$1.run(DseBackendHandler.java:167)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:53)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.948
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.DSMLTransformationService.getFunctionForLeftSideType(DSMLTransformationService.java:342)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.948
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.DSMLTransformationService.getAllocFunctionForLeftSideType(DSMLTransformationService.java:352)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.948
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.createAllocationExpression(ConstraintToNONQuantifiedSMT.java:316)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.948
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBoolean(ConstraintToNONQuantifiedSMT.java:204)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.948
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:129)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.948
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBinder(ConstraintToNONQuantifiedSMT.java:170)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.948
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:125)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.948
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMTBinder(ConstraintToNONQuantifiedSMT.java:165)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.948
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.toSMT(ConstraintToNONQuantifiedSMT.java:125)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.949
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT.transfrom(ConstraintToNONQuantifiedSMT.java:118)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.949
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.DSMLtoSMTTransformator.transform(DSMLtoSMTTransformator.java:203)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.949
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.SolverRun2.solveOptimized(SolverRun2.java:119)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.949
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.rework.DeploymentRun2.solveDeployment(DeploymentRun2.java:98)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.949
!MESSAGE
org.fortiss.af3.exploration.smt.backend.Z3Backend.executeDSE(Z3Backend.java:58)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.949
!MESSAGE
org.fortiss.af3.exploration.backend.DseBackendHandler$1.run(DseBackendHandler.java:167)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2018-03-29 19:01:08.949
!MESSAGE org.eclipse.core.internal.jobs.Worker.run(Worker.java:53)
How to reproduce.
First case:
- Load the ACC example.
- Switch to the DSE perspective and create a DSE projective for the ACC example.
- Switch to the Deployment synthesis and observe the first exception.
Second case:
- Import the attached model.
- Open the DSE perspective and select the DSE project from the attached model.
- Go to the deployment synthesis.
- Deselect the basic deployment RuleSet and select the “DSE User” RuleSet (references a single objective: Power Min.).
- Press “generate” and observe the second exception in the eclipse console.
P.S.: Urgent, since it must be fixed for the release. Not intended as pressure :)
(from redmine: issue id 3362, created on 2018-03-29, closed on 2019-01-25)
- Uploads: