Cannot save/replay CSP traces

Description

NullPointerExceptions occurs when save button is clicked in HistoryView. It happens with the machine file extension ".csp"

Environment

None

Activity

Show:
dgelessus
January 22, 2018, 2:46 PM

The problem seems to be that LoadedMachine.getMachineOperationInfo doesn't find an OperationInfo for the start_cspm_MAIN operation - maybe because it is generated by ProB and doesn't exist in the source file. I don't know enough about CSP and this part of the kernel to fix this though.

Michael Leuschel
September 27, 2018, 11:03 AM

Operation Infos are now provided for start_cspm_MAIN; saving works now but replay does not work yet:

java.lang.IllegalArgumentException: Formula must be a predicate: 1=1
at de.prob.animator.command.GetOperationByPredicateCommand.<init>(GetOperationByPredicateCommand.java:56)
at de.prob2.ui.animation.tracereplay.TraceChecker.replayPersistentTransition(TraceChecker.java:195)
at de.prob2.ui.animation.tracereplay.TraceChecker.lambda$replayTrace$5(TraceChecker.java:131)
at java.lang.Thread.run(Thread.java:748)

dgelessus
July 11, 2019, 12:20 PM

Some parts of the trace replay mechanism assume that the model uses B-like expression syntax. For example, the operation predicates are constructed using PredicateBuilder, which creates a B predicate based on a mapping of variables to values. This does not work for CSP because of syntax differences.

Also it seems that GetOperationByPredicateCommand doesn't work with CSP at all. Even if I hardcode the predicate as 1==1 (which appears to be a valid CSP expression), I get an error "Unknown Operation start_cspm_MAIN".

Fabian Vu
August 24, 2020, 2:13 PM

Deactivate saving and replaying traces for all formalisms other than B or translated to B

Assignee

Fabian Vu

Reporter

Fabian Vu

Labels

None

Priority

Minor
Configure