Internal error with model checker

[richardpaynea55]

When trying to run the model checker with a model with no unsupported syntax (SVN>Common>CaseStudies>BorderTraffic_MC), an error is given:

Could not analyse the specification.
Internal error when accessing some null object during FORMULA script generation.

Looking at the error log, it appears to be around the use of an Apply expression, but I don't know what the issue is.

[adalbertocajueiro]

That is because the model checker accepts channels with zero or one parameter. thus, channel with types T * T (or more) are not allowed. This has been added as an unsupported elements.

[ldcouto]

Just checked this and the compatibility warnings are now issued correctly.

@richardpayne , we'll have to re-rengineer the model slightly.

@adalbertocajueiro , does the MC support record types in channels?

[adalbertocajueiro]

The model checker does not support product type.

[richardpaynea55]

This issue is still present - using version 0.4.0 of Symphony. I changed the model (updated in SVN) to have channels with only one parameter, and error still occurs.

Stack trace appears to suggest a NullPointerException on MCAApplyExp.toFormula

[adalbertocajueiro]

That is because the model uses processes with more than one parameter. This is pointed out in D31.4 User manual (page 66). Due to this, the translation considers an MCApply node (a call with more than one parameter) and this throws an exception. The mc unsupported collector was adjusted to inform this (processes with more than one parameter are not allowed) before analysing the model.

[richardpaynea55]

Issue is still present. Reworked example to have no parametrised processes or actions. Can you suggest an alternative model which will go through?

Still get NullPointerException at MCAApplyExp.toFormula(MCAApplyExp.java:51)

[adalbertocajueiro]

Some classes have been modified to handle this bug and the model was adjusted to allow its analysis. Please test again and close the bug, if everything is ok.