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()
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.
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
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.
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.
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.
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.
Fixed in rev. 4370 (trunk) and rev. 4372 (4.0.9).