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

[Christian Krause <henshin.ck@xxxxxxxxx>]

Hi Subramanya,

if you open the statespace file in the statespace explorer, you can export it as an *.aut file. You can then try to run ltsconvert on that *.aut file. Make sure the statespace if completely explored.

You can also take a look at this paper which describes a bit more detailed how the Henshin-mCRL2 toolchain works:

http://www.eclipse.org/henshin/documents/henshin_mcrl2.pdf

If you are even interested in the implementation of the pipeline, you can find its Java code here:

http://dev.eclipse.org/svnroot/modeling/org.eclipse.emft.henshin/trunk/plugins/org.eclipse.emf.henshin.statespace.external/src/org/eclipse/emf/henshin/statespace/external/mcrl2/MCRL2StateSpaceValidator.java

But of course, you can also ask us here on the mailing list if you have questions or problems. It would also help if you could tell us the tool versions, your OS and how you invoke the toolchain (Java / UI) 

Cheers,
Christian

2013/9/23 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

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