search

symphonytool / symphony

The Symphony IDE
5 stars 4 forks source link

Internal error with model checker #303

Open richardpaynea55 opened 9 years ago

richardpaynea55 commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

The model checker does not support product type.

richardpaynea55 commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

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.