Skip to main content
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index] [List Home]
Re: [henshin-dev] Error while modeling checking henshin state space
Hi Christian,

As per your advice, I tried to model check the (execute  [true*]<true>true ) on dining philosopher state space and I get "pbes2bool produced no output"

java.lang.RuntimeException: pbes2bool produced no output.
    at org.eclipse.emf.henshin.statespace.external.mcrl2.MCRL2StateSpaceValidator.validate(MCRL2StateSpaceValidator.java:138)
    at org.eclipse.emf.henshin.statespace.explorer.jobs.ValidateStateSpaceJob.run(ValidateStateSpaceJob.java:54)
    at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)


and  further when I tried to execute,  ltsconvert --equivalence=bisim xxx.aut min.aut  in command line I do not see any errors(attached screen shot).


Environment am using is :
OS: Windows 7 (64 bit)
Eclipse Indigo

Please let me know where the problem is.

Thanks a lot





On Thu, Sep 26, 2013 at 3:58 PM, Subramanya K G <subramanya.kg@xxxxxxxxx> wrote:
Thanks a lot for the reply and also for the article :) . Can you also please suggest few more materials on how I can try out model checking on state space generated with henshin tool.

Thanks
Subramanya


On Thu, Sep 26, 2013 at 3:46 PM, Christian Krause <henshin.ck@xxxxxxxxx> wrote:
Ok, I will try it out myself next week.

You might be also interested in this recent article: http://ocl2013.inf.mit.bme.hu/submissions/ocl2013_submission_11.pdf

Cheers,
Christian



2013/9/26 Subramanya K G <subramanya.kg@xxxxxxxxx>
Hello Christian,

I have made no changes in the properties and Currently am trying to execute the ready-made example of "Dining philosopher"
.
Yes, while checking [true*]<true>true am getting the below error and am not able to find the reason:

pbes2bool produced no output.
pbes2bool produced no output.







On Tue, Sep 24, 2013 at 2:30 PM, Christian Krause <henshin.ck@xxxxxxxxx> wrote:
Hi Subrmany,

which property are you trying to check and how did you define of the identityTypes parameter?

Does [true*]<true>true work?

Cheers,
Christian 


2013/9/24 Subramanya K G <subramanya.kg@xxxxxxxxx>
Hi Christian,

I re installed mCRL2. Now on checking constraint in the Validation window, I got the below error:


pbes2bool produced no output.
pbes2bool produced no output.


and also the below error on executing the examples given in the eclipse henshin tutorial.

lps2pbes returned exit code 1:

[12:08:17 error]   basic or defined sort Fork is not declared
[12:08:17 error]   could not type check modal formula TEMPORARILY IN ATERM FORMATStateMust(RegTransOrNil(ActTrue),StateForall([DataVarId(f1,SortId(Fork)),DataVarId(f2,SortId(Fork))],StateExists([DataVarId(p,SortId(Philosopher))],StateMust(RegSeq(UntypedActMultAct([UntypedAction(left,[UntypedIdentifier(p),UntypedIdentifier(f1)])]),UntypedActMultAct([UntypedAction(right,[UntypedIdentifier(p),UntypedIdentifier(f2)])])),StateNu(X,[],StateMu(Y,[],StateAnd(StateMust(UntypedActMultAct([UntypedAction(release,[UntypedIdentifier(p),UntypedIdentifier(f1),UntypedIdentifier(f2)])]),StateVar(X,[])),StateMust(ActNot(UntypedActMultAct([UntypedAction(release,[UntypedIdentifier(p),UntypedIdentifier(f1),UntypedIdentifier(f2)])])),StateVar(Y,[])))))))))
lps2pbes returned exit code 1:

[12:08:17 error]   basic or defined sort Fork is not declared
[12:08:17 error]   could not type check modal formula TEMPORARILY IN ATERM FORMATStateMust(RegTransOrNil(ActTrue),StateForall([DataVarId(f1,SortId(Fork)),DataVarId(f2,SortId(Fork))],StateExists([DataVarId(p,SortId(Philosopher))],StateMust(RegSeq(UntypedActMultAct([UntypedAction(left,[UntypedIdentifier(p),UntypedIdentifier(f1)])]),UntypedActMultAct([UntypedAction(right,[UntypedIdentifier(p),UntypedIdentifier(f2)])])),StateNu(X,[],StateMu(Y,[],StateAnd(StateMust(UntypedActMultAct([UntypedAction(release,[UntypedIdentifier(p),UntypedIdentifier(f1),UntypedIdentifier(f2)])]),StateVar(X,[])),StateMust(ActNot(UntypedActMultAct([UntypedAction(release,[UntypedIdentifier(p),UntypedIdentifier(f1),UntypedIdentifier(f2)])])),StateVar(Y,[])))))))))



Many thanks


On Tue, Sep 24, 2013 at 11:48 AM, Subramanya K G <subramanya.kg@xxxxxxxxx> wrote:
Hello Christian,

Thank you for the reply, I will go through the papers too.

Also I go the error as shown below (i.e. a dll file is missing), I will reinstall and try.

Thank You
Subu


On Mon, Sep 23, 2013 at 6:44 PM, Christian Krause <henshin.ck@xxxxxxxxx> wrote:
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:

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

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



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




--


Thanks & Regards,
Subramanya



--


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



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




--


Thanks & Regards,
Subramanya



--


Thanks & Regards,
Subramanya

Attachment: cmd.png
Description: PNG image

Back to the top