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 Subramany,

you are attempting to check a property with actions without parameters. If you use the example as it is defined in the examples plugin, it does have parameters: all rules have a parameter for the matched philosopher.

There are two ways to fix it:

1) Edit the rules and remove their parameters (click twice on the rule name and just remove everything in the brackets). Then you can use your formula as is.

2) The other way is to add parameters to the actions in the formula. Maybe take a look at the Wiki page to see how this works.

Hope that helps,
Christian



2013/10/16 Subramanya K G <subramanya.kg@xxxxxxxxx>
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

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


Back to the top