This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 477 - Unstable verification result and segmentation fault in server
Summary: Unstable verification result and segmentation fault in server
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.8
Hardware: PC Linux
: P2 critical
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2009-07-09 10:24 CEST by Mikkel Koefoed Jakobsen
Modified: 2009-08-07 12:41 CEST (History)
0 users

See Also:
Architecture:


Attachments
Models (17.51 KB, text/xml)
2009-07-09 10:30 CEST, Mikkel Koefoed Jakobsen
Details
The queries for the model (3.27 KB, application/octet-stream)
2009-07-09 10:32 CEST, Mikkel Koefoed Jakobsen
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Mikkel Koefoed Jakobsen 2009-07-09 10:24:22 CEST
For certain queries the results are unstable (i.e. "Property is satisfied.", "Property is not satisfied." and Unexpected server crash/segmentation fault).

This is best reproducible with "Reuse" turned off, all other options are at their default (Produced with UPPAAL 4.0.8 (rev. 4276), March 2009).

The queries that produce these unstable results are:
nodes(1).UpdateEnergy --> nodes(1).hasValidRoute()
nodes(2).UpdateEnergy --> nodes(2).hasValidRoute()
nodes(3).UpdateEnergy --> nodes(3).hasValidRoute()
nodes(4).UpdateEnergy --> nodes(4).hasValidRoute()
Comment 1 Mikkel Koefoed Jakobsen 2009-07-09 10:30:40 CEST
Created attachment 222 [details]
Models

Simple model of a wireless sensor network:

"Environment" produce energy for the nodes.
"BaseStation" collects all packages routed to sink.
"Node" produce packages through the "Application" and route packages through the network. Nodes also model a dynamic routing protocol which modify the routes based on available energy in neighbouring nodes.

The system consists of one base station, four nodes and an environment. The nodes are positioned as following (0 is the base station):

0 - 1 - 2 - 3
        |
        4

the lines represent radio connections (synchronisations). The nodes uses channels for routing packages and broadcast channels for updating information about neighbours.
Comment 2 Mikkel Koefoed Jakobsen 2009-07-09 10:32:36 CEST
Created attachment 223 [details]
The queries for the model

The interesting queries are:

nodes(1).UpdateEnergy --> nodes(1).hasValidRoute()
nodes(2).UpdateEnergy --> nodes(2).hasValidRoute()
nodes(3).UpdateEnergy --> nodes(3).hasValidRoute()
nodes(4).UpdateEnergy --> nodes(4).hasValidRoute()

which give a new result for each verification with the stable release 4.0.8
Comment 3 Mikkel Koefoed Jakobsen 2009-07-09 10:34:17 CEST
When trying to reproduce the bug with the latest developer version (UPPAAL 4.1.1 (rev. 4276), March 2009) the server crashes/segfaults every time.
Comment 4 Mikkel Koefoed Jakobsen 2009-07-09 10:39:32 CEST
Using the command line verifyta produce the same results as through the GUI (for both the stable release and the developer version respectively).

i.e.: 
(Academic) UPPAAL 4.0.8 (rev. 4276), March 2009
Copyright (c) 1995 - 2009, Uppsala University and Aalborg University.
All rights reserved.
Compiled with g++-4.3.3 -Wall -DNDEBUG -O3 -ffloat-store -fgcse-las -fgcse-lm -fgcse-sm -ftree-loop-linear -funswitch-loops -ftree-loop-im -fivopts -ftree-vectorize -ftracer -march=pentiumpro -DLIBXML_STATIC    -DBOOST_DISABLE_THREADS
Free for academic and non-commercial use only.

produce either of:
 -- Property is satisfied.
 -- Property is NOT satisfied.
segmentation fault

-------------------
(Academic) UPPAAL 4.1.1 (rev. 4276), March 2009
Copyright (c) 1995 - 2009, Uppsala University and Aalborg University.
All rights reserved.
Compiled with g++-4.3.3 -Wall -DNDEBUG -O3 -ffloat-store -fgcse-las -fgcse-lm -fgcse-sm -ftree-loop-linear -funswitch-loops -ftree-loop-im -fivopts -ftree-vectorize -ftracer -march=pentiumpro -DLIBXML_STATIC -DENABLE_ROBUST_REACHABILITY -DENABLE_CSS_MERGE    -DBOOST_DISABLE_THREADS
Free for academic and non-commercial use only.

constantly produce segmentation fault.
Comment 5 Mikkel Koefoed Jakobsen 2009-07-09 10:43:01 CEST
By the way: when I wrote all other options are at their default, i mean that I use:
Search order: Breath first
State space reduction: Conservative
State space representation: DBM
Diagnostic trace: None
Extrapolation: Automatic
Hash table size: 16M
Reuse: Off

This is true for all the tested versions.
Comment 6 Alexandre David 2009-08-04 17:51:46 CEST
The problem has been identified although no fix is currently available.

Avoid using sub-expressions in queries of the form name(index).call(arg)
where "name" is a process name (of a process set), "index" some index (constant
or not), "call" a function name local to the process, and "arg" its
arguments. Other references like locations or variables are fine. Just
avoid calling local functions for the time being.
Comment 7 Alexandre David 2009-08-07 12:41:01 CEST
Fixed in rev. 4370 (trunk) and rev. 4372 (4.0.9).