Project

General

Profile

Bug #3520

nuxmv problme on STL

Added by Anonymous about 2 years ago. Updated almost 2 years ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
09/17/2018
Due date:
% Done:

0%

Estimated time:

Description

!ENTRY org.fortiss.af3.specification 4 0 2018-09-17 16:58:11.000
!MESSAGE
!STACK 0
java.lang.NullPointerException
at org.fortiss.af3.state.generator.nusmv.CopyProject.transform(CopyProject.java:58)
at org.fortiss.pragmatictransformation.service.CacheSupportedTransformationBase.buildTransformation(CacheSupportedTransformationBase.java:45)
at org.fortiss.pragmatictransformation.service.CompositionTransformation$Simultaneous.buildTransformation(CompositionTransformation.java:90)
at org.fortiss.pragmatictransformation.service.CompositionTransformation$Sequence.buildTransformation(CompositionTransformation.java:56)
at org.fortiss.pragmatictransformation.service.CompositionTransformation$Sequence.buildTransformation(CompositionTransformation.java:56)
at org.fortiss.pragmatictransformation.service.PragmaticTransformationBase.buildTransformation(PragmaticTransformationBase.java:27)
at org.fortiss.af3.specification.modelchecking.af3tonusmv.ReachabilityAnalyzer$StateReachabilitySpecification.lambda$1(ReachabilityAnalyzer.java:126)
at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
at java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1382)
at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:708)
at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:499)
at org.fortiss.af3.tools.nusmv.model.NuSMVModelFactory.createSetDefinition(NuSMVModelFactory.java:220)
at org.fortiss.af3.specification.modelchecking.af3tonusmv.ReachabilityAnalyzer$StateReachabilitySpecification.createReachabilitySpecification(ReachabilityAnalyzer.java:125)
at org.fortiss.af3.specification.modelchecking.af3tonusmv.ReachabilityAnalyzer.lambda$1(ReachabilityAnalyzer.java:79)
at java.util.ArrayList.forEach(ArrayList.java:1257)
at org.fortiss.af3.specification.modelchecking.af3tonusmv.ReachabilityAnalyzer.checkAllStatesReachable(ReachabilityAnalyzer.java:78)
at org.fortiss.af3.specification.constraint.ReachabilityConstraint.concreteVerify(ReachabilityConstraint.java:60)
at org.fortiss.af3.specification.constraint.StateAutomatonConstraintBase.concreteVerify(StateAutomatonConstraintBase.java:60)
at org.fortiss.af3.specification.constraint.AbstractFormalVerificationConstraint.verify(AbstractFormalVerificationConstraint.java:76)
at org.fortiss.tooling.kernel.internal.ConstraintService.lambda$0(ConstraintService.java:143)
at org.fortiss.tooling.kernel.internal.storage.eclipse.ModelContext$2.execute(ModelContext.java:435)
at org.fortiss.tooling.kernel.internal.storage.eclipse.EMFTransactionalCommand$1.doExecute(EMFTransactionalCommand.java:55)
at org.eclipse.emf.transaction.RecordingCommand.execute(RecordingCommand.java:135)
at org.fortiss.tooling.kernel.internal.storage.eclipse.EMFTransactionalCommand$2.run(EMFTransactionalCommand.java:67)
at org.fortiss.tooling.kernel.internal.storage.eclipse.EMFTransactionalCommand.runInTransaction(EMFTransactionalCommand.java:99)
at org.fortiss.tooling.kernel.internal.storage.eclipse.EMFTransactionalCommand.execute(EMFTransactionalCommand.java:64)
at org.eclipse.emf.common.command.BasicCommandStack.execute(BasicCommandStack.java:78)
at org.eclipse.emf.transaction.impl.AbstractTransactionalCommandStack.basicExecute(AbstractTransactionalCommandStack.java:241)
at org.eclipse.emf.transaction.impl.TransactionalCommandStackImpl.doExecute(TransactionalCommandStackImpl.java:63)
at org.eclipse.emf.transaction.impl.AbstractTransactionalCommandStack.execute(AbstractTransactionalCommandStack.java:165)
at org.eclipse.emf.transaction.impl.AbstractTransactionalCommandStack.execute(AbstractTransactionalCommandStack.java:219)
at org.fortiss.tooling.kernel.internal.storage.eclipse.AutoUndoCommandStack.execute(AutoUndoCommandStack.java:79)
at org.fortiss.tooling.kernel.internal.storage.eclipse.ModelContext.runAsCommand(ModelContext.java:426)
at org.fortiss.tooling.kernel.internal.ConstraintService.verify(ConstraintService.java:139)
at org.fortiss.tooling.kernel.ui.extension.base.ConstraintUIBases$ConstraintUIBaseAutocheck$1.run(ConstraintUIBases.java:242)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:53)

History

#1 Updated by Anonymous almost 2 years ago

  • Status changed from New to Resolved
  • Assignee changed from Anonymous to Anonymous
  • Target version set to AF3 2.15 RC2 (Tested, Bug-free)

Should have been resolved. I tried to run few analyses on STL and did not get this exception anymore.

#2 Updated by Anonymous almost 2 years ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF