If I take the standard ChoiceSupportinDebugger project and try to set the preference so it makes use of the ProB backend for solving and start the debugger I get:
Waiting for environment on : tau, tock
Waiting for environment on : tock, tau
Waiting for environment on : tock, tau
---------------------------------------------------------------------------------
Solver running for operation: rndElement
Solver input:
v~:POW(INT) &
v:POW(INT) &
r:s &
s={1,2,3,4}
org.overture.modelcheckers.probsolver.AbstractProbSolverUtil$SolverException: Internal error in solver invocation
at org.overture.modelcheckers.probsolver.ProbSolverUtil.solve(ProbSolverUtil.java:423)
at org.overture.modelcheckers.probsolver.ProbSolverUtil.solve(ProbSolverUtil.java:357)
at org.overture.modelcheckers.probsolver.ProbSolverUtil.solve(ProbSolverUtil.java:110)
at org.overture.modelcheckers.probsolver.ProbSolverIntegration.solve(ProbSolverIntegration.java:36)
at org.overture.interpreter.values.FunctionValue.invokeSolver(FunctionValue.java:633)
at org.overture.interpreter.values.FunctionValue.eval(FunctionValue.java:479)
at org.overture.interpreter.values.FunctionValue.eval(FunctionValue.java:276)
at org.overture.interpreter.eval.ExpressionEvaluator.caseAApplyExp(ExpressionEvaluator.java:143)
at org.overture.interpreter.eval.ExpressionEvaluator.caseAApplyExp(ExpressionEvaluator.java:119)
at org.overture.ast.expressions.AApplyExp.apply(AApplyExp.java:385)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor$VdmExpressionEvaluator.defaultPExp(CmlExpressionVisitor.java:83)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor.defaultPExp(CmlExpressionVisitor.java:111)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor.defaultPExp(CmlExpressionVisitor.java:54)
at org.overture.ast.analysis.QuestionAnswerAdaptor.caseAApplyExp(QuestionAnswerAdaptor.java:622)
at org.overture.ast.expressions.AApplyExp.apply(AApplyExp.java:385)
at org.overture.interpreter.eval.StatementEvaluator.caseAAssignmentStm(StatementEvaluator.java:145)
at org.overture.interpreter.eval.StatementEvaluator.caseAAssignmentStm(StatementEvaluator.java:105)
at org.overture.ast.statements.AAssignmentStm.apply(AAssignmentStm.java:491)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor.defaultPStm(CmlExpressionVisitor.java:104)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor.defaultPStm(CmlExpressionVisitor.java:54)
at org.overture.ast.analysis.QuestionAnswerAdaptor.caseAAssignmentStm(QuestionAnswerAdaptor.java:3182)
at org.overture.ast.statements.AAssignmentStm.apply(AAssignmentStm.java:491)
at org.overture.interpreter.assistant.statement.SSimpleBlockStmAssistantInterpreter.evalBlock(SSimpleBlockStmAssistantInterpreter.java:31)
at org.overture.interpreter.eval.StatementEvaluator.caseABlockSimpleBlockStm(StatementEvaluator.java:860)
at org.overture.interpreter.eval.StatementEvaluator.caseABlockSimpleBlockStm(StatementEvaluator.java:105)
at org.overture.ast.statements.ABlockSimpleBlockStm.apply(ABlockSimpleBlockStm.java:268)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor.defaultPStm(CmlExpressionVisitor.java:104)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor.defaultPStm(CmlExpressionVisitor.java:54)
at org.overture.ast.analysis.QuestionAnswerAdaptor.defaultSSimpleBlockStm(QuestionAnswerAdaptor.java:3372)
at org.overture.ast.analysis.QuestionAnswerAdaptor.caseABlockSimpleBlockStm(QuestionAnswerAdaptor.java:3482)
at org.overture.ast.statements.ABlockSimpleBlockStm.apply(ABlockSimpleBlockStm.java:268)
at org.overture.interpreter.assistant.statement.SSimpleBlockStmAssistantInterpreter.evalBlock(SSimpleBlockStmAssistantInterpreter.java:31)
at org.overture.interpreter.eval.StatementEvaluator.caseABlockSimpleBlockStm(StatementEvaluator.java:860)
at org.overture.interpreter.eval.StatementEvaluator.caseABlockSimpleBlockStm(StatementEvaluator.java:105)
at org.overture.ast.statements.ABlockSimpleBlockStm.apply(ABlockSimpleBlockStm.java:268)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor.defaultPStm(CmlExpressionVisitor.java:104)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor.defaultPStm(CmlExpressionVisitor.java:54)
at org.overture.ast.analysis.QuestionAnswerAdaptor.defaultSSimpleBlockStm(QuestionAnswerAdaptor.java:3372)
at org.overture.ast.analysis.QuestionAnswerAdaptor.caseABlockSimpleBlockStm(QuestionAnswerAdaptor.java:3482)
at org.overture.ast.statements.ABlockSimpleBlockStm.apply(ABlockSimpleBlockStm.java:268)
at org.overture.interpreter.values.OperationValue.localEval(OperationValue.java:422)
at org.overture.interpreter.values.OperationValue.eval(OperationValue.java:276)
at org.overture.interpreter.eval.ExpressionEvaluator.caseAApplyExp(ExpressionEvaluator.java:154)
at org.overture.interpreter.eval.ExpressionEvaluator.caseAApplyExp(ExpressionEvaluator.java:119)
at org.overture.ast.expressions.AApplyExp.apply(AApplyExp.java:385)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor$VdmExpressionEvaluator.defaultPExp(CmlExpressionVisitor.java:83)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor.defaultPExp(CmlExpressionVisitor.java:111)
at eu.compassresearch.core.interpreter.CmlExpressionVisitor.defaultPExp(CmlExpressionVisitor.java:54)
at org.overture.ast.analysis.QuestionAnswerAdaptor.caseAApplyExp(QuestionAnswerAdaptor.java:622)
at org.overture.ast.expressions.AApplyExp.apply(AApplyExp.java:385)
at eu.compassresearch.core.interpreter.StatementInspectionVisitor.evalSingleAssignmentStatement(StatementInspectionVisitor.java:446)
at eu.compassresearch.core.interpreter.StatementInspectionVisitor.access$000(StatementInspectionVisitor.java:53)
at eu.compassresearch.core.interpreter.StatementInspectionVisitor$14.execute(StatementInspectionVisitor.java:415)
at eu.compassresearch.core.interpreter.ConcreteCmlBehaviour.execute(ConcreteCmlBehaviour.java:329)
at eu.compassresearch.core.interpreter.CommonInspectionVisitor$30.execute(CommonInspectionVisitor.java:1070)
at eu.compassresearch.core.interpreter.ConcreteCmlBehaviour.execute(ConcreteCmlBehaviour.java:329)
at eu.compassresearch.core.interpreter.CommonInspectionVisitor$7.execute(CommonInspectionVisitor.java:334)
at eu.compassresearch.core.interpreter.ConcreteCmlBehaviour.execute(ConcreteCmlBehaviour.java:329)
at eu.compassresearch.core.interpreter.VanillaCmlInterpreter.executeBehaviour(VanillaCmlInterpreter.java:282)
at eu.compassresearch.core.interpreter.VanillaCmlInterpreter.executeTopProcess(VanillaCmlInterpreter.java:239)
at eu.compassresearch.core.interpreter.VanillaCmlInterpreter.execute(VanillaCmlInterpreter.java:166)
at eu.compassresearch.core.interpreter.debug.SocketServerCmlDebugger.start(SocketServerCmlDebugger.java:434)
at eu.compassresearch.core.interpreter.debug.DebugMain.main(DebugMain.java:204)
Caused by: com.google.inject.ProvisionException: Guice provision errors:
1) Error in custom provider, java.lang.NullPointerException
while locating de.prob.cli.ProBInstanceProvider
while locating de.prob.cli.ProBInstance
for parameter 0 at de.prob.animator.AnimatorImpl.<init>(AnimatorImpl.java:40)
while locating de.prob.animator.AnimatorImpl
while locating de.prob.animator.IAnimator
1 error
at com.google.inject.internal.InjectorImpl$4.get(InjectorImpl.java:987)
at com.google.inject.internal.InjectorImpl.getInstance(InjectorImpl.java:1013)
at org.overture.modelcheckers.probsolver.AbstractProbSolverUtil.initialize(AbstractProbSolverUtil.java:172)
at org.overture.modelcheckers.probsolver.ProbSolverUtil.solve(ProbSolverUtil.java:369)
... 62 more
Caused by: java.lang.NullPointerException
at de.prob.cli.ProBInstanceProvider.startProlog(ProBInstanceProvider.java:59)
at de.prob.cli.ProBInstanceProvider.create(ProBInstanceProvider.java:50)
at de.prob.cli.ProBInstanceProvider.get(ProBInstanceProvider.java:38)
at de.prob.cli.ProBInstanceProvider.get(ProBInstanceProvider.java:25)
at com.google.inject.internal.BoundProviderFactory.get(BoundProviderFactory.java:55)
at com.google.inject.internal.SingleParameterInjector.inject(SingleParameterInjector.java:38)
at com.google.inject.internal.SingleParameterInjector.getAll(SingleParameterInjector.java:62)
at com.google.inject.internal.ConstructorInjector.construct(ConstructorInjector.java:84)
at com.google.inject.internal.ConstructorBindingImpl$Factory.get(ConstructorBindingImpl.java:254)
at com.google.inject.internal.FactoryProxy.get(FactoryProxy.java:54)
at com.google.inject.internal.InjectorImpl$4$1.call(InjectorImpl.java:978)
at com.google.inject.internal.InjectorImpl.callInContext(InjectorImpl.java:1024)
at com.google.inject.internal.InjectorImpl$4.get(InjectorImpl.java:974)
... 65 more
Terminated
Error 4066: Cannot call implicit operation: rndElement in 'C:\TEMP\SymphonyIDE\workspace\ChoiceSupportInDebugger\Choice.cml' at line 15:40 at in 'C:\TEMP\SymphonyIDE\workspace\ChoiceSupportInDebugger\Choice.cml' at line 15:40
If I take the standard ChoiceSupportinDebugger project and try to set the preference so it makes use of the ProB backend for solving and start the debugger I get: