Getting "Server connection lost" error

[phd150...@iiti.ac.in]

I use Uppaal version 4.1.19 on Ubuntu 16.04 with Java 1.8.0_91.

Hello,
I am using Uppaal SMC for verifying a statistical property. There is no syntactic error in the model. However, when I run the property in the verifier, it shows an error message saying "Server connection lost". I am not sure what could the problem be. I will appreciate any help in this regard.

Thanks,
Aaditya

[Marius Mikučionis]

Hi,

On Tuesday, January 7, 2020 at 7:06:23 AM UTC+1, Aditya Prakash Chouhan wrote:

I use Uppaal version 4.1.19 on Ubuntu 16.04 with Java 1.8.0_91.

Is there a reason for not upgrading Uppaal?

 

Hello,
I am using Uppaal SMC for verifying a statistical property. There is no syntactic error in the model. However, when I run the property in the verifier, it shows an error message saying "Server connection lost". I am not sure what could the problem be. I will appreciate any help in this regard.

Looks like an engine crash (bug), I need more details to reproduce it.

Could you try a newer version? Perhaps this issue has already been fixed.

Best regards,
Marius

[Aditya Prakash Chouhan]

Hello, 

Thanks for replying. I have tried that with the Uppaal 4.1.24 as well, it gives the same error message. I am attaching the error message that I am getting on Uppaal 4.1.24 as well as the message on the terminal. Please let me know of any information that you need in addition to this. 

[Marius Mikučionis]

Hi,

On Tuesday, January 7, 2020 at 10:02:37 AM UTC+1, Aditya Prakash Chouhan wrote:

Hello, 

Thanks for replying. I have tried that with the Uppaal 4.1.24 as well, it gives the same error message. I am attaching the error message that I am getting on Uppaal 4.1.24 as well as the message on the terminal. Please let me know of any information that you need in addition to this. 

OK, I tried a query similar to yours and it works.

I suspect that there is something in the model that triggers this crash.

Could you send me the model?

Alternatively, you could try the concrete simulator and see which transition crashes the engine.

(the concrete simulator should work if there are no ODEs in the model)

Best regards,
Marius

[susann...@gmail.com]

I also get this "server connection lost" error, but only rarely, for some requirements. Everything is ok for hundreds of requests, but now I changed slightly a property, and I get constantly this same error.

First I tried
(Thread(1).endT3 && Thread(1).x == 159) --> (Thread(1).endT3 && Thread(1).x == 159)
as an alternative to infinitely often "this predicate p". Unfortunately this is of course trivially true ... so not of much help. Therefore, I tried a weaker but still relevant property:
(Thread(1).endT3 && Thread(1).x == 159) --> (Thread(0).endT3 && Thread(0).x == 159)
and for this one (for which I would really like to get an answer) I get (almost immediatly) this server connection lost error.
Note that no state explosion shoul occur because I check without any problem tons of properties on exactly the same model

Susanne Graf

[Marius Mikučionis]

Dear Susanne Graf,

Could you please share your model with me?

I have tried the queries and they seem to work, i.e. nothing special about them, so I suspect that there is something in the model that triggers the issue.

I tried creating processes for various ranges, accessing non-existent instances -- it just works, I am running out of imagination and need your help to reproduce it.

The symptoms that you are describing are very general: the engine simply crashes and that's it.

Usually it is easy to spot and fix such issues provided that the crash is reproduced.

As usual, I promise not to share the model with anyone else.

Best regards,

Marius

[noraf...@googlemail.com]

Hi Marius, hi all,

I have the same error (SercerException: Server connection lost) when simulating/verifying although the same model is working on my colleagues computer.

Has there been a solution to this message?

Thanks!
Nora

[Susanne Graf]

Hi Nora,

in my case the problem was proving liveness properties in the presence of
priorities. Apparently they do not necessarily work together well.

Eliminating the priority rules (which where there just for optimization reasons)
or downgrading properties to safety (using an observer) eliminated the problem.

But this seems not to be your problem.

In fact, on a different model, I had also an issue with using an old releas if
my memory is good enough. Using 4.1.24 release solved (at least some of) the
problems

best regards
Susanne

--
------------------------------------------------------------------------
Susanne Graf | tel : +33 4 57 42 22 19
VERIMAG - Bâtiment IMAG | http://www-verimag.imag.fr/~graf/
700 avenue Centrale DU | e-mail: Susann...@imag.fr
F - 38401 St Martin d’Hères
------------------------------------------------------------------------

[noraf...@googlemail.com]

Susanne, thank you for reply, much appreciated! I am using 4.1.24, so I am still on the quest for the solution.

Thanks!

[Marius Mikučionis]

Dear Nora,

On Tuesday, 4 August 2020 14:49:04 UTC+2, norafranzen wrote:

Susanne, thank you for reply, much appreciated! I am using 4.1.24, so I am still on the quest for the solution.

 

I presume that you are not using priorities with liveness property (which caused the original issue).

If so, I would be very much interested to look at your model and hopefully fix Uppaal.

Best regards,

Marius

Thanks!

On Tuesday, July 28, 2020 at 9:28:32 PM UTC+2, Susanne Graf wrote:
> Hi Nora,
>
> in my case the problem was proving liveness properties in the presence of
> priorities. Apparently they do not necessarily work together well.
>
> Eliminating the priority rules (which where there just for optimization reasons)
> or downgrading properties to safety (using an observer) eliminated the problem.
>
> But this seems not to be your problem.
>
> In fact, on a different model, I had  also an issue with using an old releas if
> my memory is good enough. Using 4.1.24 release solved (at least some of) the
> problems
>
> best regards
> Susanne
>
> On 28/07/2020 13:53, norafranzen via UPPAAL wrote:
> > Hi Marius, hi all,
> >
> > I have the same error (SercerException: Server connection lost) when simulating/verifying although the same model is working on my colleagues computer.
> >
> > Has there been a solution to this message?
> >
> > Thanks!
> > Nora
> >
>
> --
> ------------------------------------------------------------------------
> Susanne Graf                | tel : +33 4 57 42 22 19
> VERIMAG - Bâtiment IMAG     | http://www-verimag.imag.fr/~graf/
> 700 avenue Centrale DU      | e-mail: