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,

I was checking the example: 
<true*>nu X.<left.right.release>X on dining philosopher state space and encountered the below error. 


[12:41:15 error]   no action release with 0 parameters is declared (while typechecking UntypedAction(release,[]))

[12:41:15 error]   while typechecking TEMPORARILY PRINT AN ATERM StateNu(X,[],StateMay(RegSeq(UntypedActMultAct([UntypedAction(left,[])]),RegSeq(UntypedActMultAct([UntypedAction(right,[])]),UntypedActMultAct([UntypedAction(release,[])]))),StateVar(X,[])))

[12:41:15 error]   could not type check modal formula TEMPORARILY IN ATERM FORMATStateMay(RegTransOrNil(ActTrue),StateNu(X,[],StateMay(RegSeq(UntypedActMultAct([UntypedAction(left,[])]),RegSeq(UntypedActMultAct([UntypedAction(right,[])]),UntypedActMultAct([UntypedAction(release,[])]))),StateVar(X,[])))



I observed that the size of the *.PBES file is Zero. So I feel there is some problem on pbes file generation.



Could you please let me know what is the problem or if I have missed out anything ??


Environment: Windows 7, mCRL2 tool.
Thanks
Subramanya


On Fri, Oct 11, 2013 at 10:54 PM, Subramanya K G <subramanya.kg@xxxxxxxxx> wrote:
Thanks a lot. Will check it tomorrow.

Thanks
Subramanya


On Fri, Oct 11, 2013 at 3:53 PM, Christian Krause <henshin.ck@xxxxxxxxx> wrote:
Hi Subramanya,

yes, mCRL2 changed the output of the pbes2bool tool. I fixed the problem in the MCRL2StateSpaceValidator class. I will commit the bugfix tonight. So tomorrow it should work using the nightly build or the source code version.

Thanks for helping finding and fixing this bug.

Cheers,
Christian


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

Thanks a lot for immediate reply. Yes I do use windows based system.

The variable "line" contains only the value false nothing other than that.

I have also attached MCRL2StateSpaceValidator.txt.

Thanks
Subramanya






On Thu, Oct 10, 2013 at 2:43 PM, Christian Krause <henshin.ck@xxxxxxxxx> wrote:
I think it is a windows problem. Windows does not have an error stream, so we should rather use the input stream then. Do you have a working solution now? What you can do for debugging is to just print the content of the "line" variable to see the output of mCRL2. If you have a working version, please send me your version. Otherwise I have to look into it later.

Cheers,
Christian


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

Thanks for the reply. I debugged the MCRL2StateSpaceValidator.java file. I noticed the below :

1. In the method -  public ValidationResult validate(StateSpace stateSpace, IProgressMonitor monitor) throws Exception { ... }
   
Line number - 100
BufferedReader reader = new BufferedReader(new InputStreamReader(process.getErrorStream()));

I noticed that process.getErrorStream() has a null value and I doubt if it has to be process.getInputStream().

Also noticed that on changing to process.getInputStream() the line will contain false value which is correct (because on executing [true*]<true>true,  the value has to be false), but

the result variable will not contain the value TRUE or FALSE because the check,

int index = line.indexOf("The solution for the initial variable of the pbes is"); is not found in the file.


Kindly look into whenever you have time. I would like to thank you very much for the help. This is helping me a lot for Master Thesis.


Thanks Once again,
Subramanya




On Wed, Oct 9, 2013 at 8:55 AM, Christian Krause <henshin.ck@xxxxxxxxx> wrote:
Hi Subramanya,

sorry, but I'm quite busy in the moment. If you have the source code, you could try to debug it. The mCRL2 model checking is done in the MCRL2StateSpaceValidator class:


I will no be able to look into it before next week.

Cheers,
Christian



2013/10/6 Subramanya K G <subramanya.kg@xxxxxxxxx>
Hello Christian,

I am still not able to execute, the same error persists.  I even tried to execute in command prompt but no success. (FYI:  I checked out the latest code).

Thanks
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

_______________________________________________
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

Back to the top