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


Back to the top