Re: [henshin-dev] Error while modeling checking henshin state space

[Subramanya K G <subramanya.kg@xxxxxxxxx>]

Hello Christian,

Thanks a lot for the quick reply, but am not able to find this file which is generated by the model checker tool.

Any possible reason for this??

Thanks

Subramanya

On Mon, Sep 23, 2013 at 1:49 PM, Christian Krause <henshin.ck@xxxxxxxxx> wrote:

Hi Subramanya,

the model checker tool generates a *.aut file in your system's temporary folder. If the file name is, say, xxx.aut then try to run this command on the command line:

ltsconvert --equivalence=bisim xxx.aut min.aut

and check if you get any error messages.

Cheers,

Christian

2013/9/23 Subramanya K G <subramanya.kg@xxxxxxxxx>

hello,

I am getting the below error when trying to model check the state space of dining philosopher example using mCRL2 tool.

Please help.

java.lang.RuntimeException: ltsconvert returned exit code -1073741515:

    at org.eclipse.emf.henshin.statespace.external.AbstractFileBasedValidator.convertFile(AbstractFileBasedValidator.java:231)

    at org.eclipse.emf.henshin.statespace.external.mcrl2.MCRL2StateSpaceValidator.validate(MCRL2StateSpaceValidator.java:69)

    at org.eclipse.emf.henshin.statespace.explorer.jobs.ValidateStateSpaceJob.run(ValidateStateSpaceJob.java:54)

    at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)

--

Thanks & Regards,
Subramanya

_______________________________________________
henshin-dev mailing list
henshin-dev@xxxxxxxxxxx
https://dev.eclipse.org/mailman/listinfo/henshin-dev

_______________________________________________
henshin-dev mailing list
henshin-dev@xxxxxxxxxxx
https://dev.eclipse.org/mailman/listinfo/henshin-dev

--

Thanks & Regards,
Subramanya