Bug 234 - Problem with verifyta
Summary: Problem with verifyta
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.6 Alpha 2
Hardware: PC Linux
: P1 blocker
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2005-12-04 22:26 CET by Venkita Subramonian
Modified: 2005-12-05 09:46 CET (History)
0 users

See Also:
Architecture:


Attachments
Test case (XML) (792 bytes, text/xml)
2005-12-05 09:21 CET, Gerd Behrmann
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Venkita Subramonian 2005-12-04 22:26:06 CET
It looks like the following model does not work as expected when using verifyta.
It works ok in the GUI simulator. I have a global state variable (my_state)
which is a structure that contains another structure as its member. This member
structure in turn is another structure which contains an array of yet another
structure. I try to add an element to this array member thru a function. 
Basically I am expecting the state to be as follows after I call the init_func(). 

my_state.astruct_set.members[0].handle=2 

This is true when I run the GUI simulator. But when I run verifyta as follows

verifyta -N -d -t 1 verify_ta_test.xta verify_ta_test.q

I get the following in the trace 

State:
( P0.S1 )
my_state.astruct_set.members[0].handle=0 .....
my_state.astruct_set.currsize=0...
Transitions:
  P0.S1->P0.S0 { 1, tau, i := init_func() }

State:
( P0.S0 )
my_state.astruct_set.members[0].handle=3 .....
my_state.astruct_set.currsize=0...

Note that the value of the handle member is 3 rather than 2
and the value of the currsize member is still 0 rather than 1.

verify_ta_test.xta
===================

typedef struct
{
  int handle;
} AStruct;

typedef struct
{
  AStruct members[5];
  int currsize;
} AStruct_Set;

typedef struct 
{
  AStruct_Set astruct_set;
} My_State;

My_State my_state;

int add_to_set(AStruct_Set& set, AStruct astruct)
{
  set.members[set.currsize] = astruct;
  ++(set.currsize);
  return 0;
}

AStruct astruct = {2};

int init_func()
{
  add_to_set(my_state.astruct_set, astruct);
  return 0;
}


process P0() {
int i;state Final, S0, S1;
init S1;
trans S0 -> Final {  },
S1 -> S0 { assign i = init_func();  };
}
//Insert process assignments.

//Edit system definition.
system P0;

verify_test_ta.q
================
E<> P0.Final
Comment 1 Gerd Behrmann 2005-12-05 09:01:19 CET
Very peculiar indeed. 99% of the code behind the server used by the GUI and verifyta is identical. Initially I 
thought this might be a duplicate of bug 223, but this does not seem to be the case (adding the -C option 
does not change anything).
Comment 2 Gerd Behrmann 2005-12-05 09:12:56 CET
The good news is that it seems to be fixed on the trunk. I suspect that the changes to bug 227 also fixed 
this problem, but I will investigate further to make sure that this is indeed the case.
Comment 3 Gerd Behrmann 2005-12-05 09:21:26 CET
Created attachment 77 [details]
Test case (XML)

Attached a smaller test case. The query is the same as above.
Comment 4 Gerd Behrmann 2005-12-05 09:41:57 CET
With the testcase I attached, the GUI shows the exact same problem. Thus it is not specific to verifyta.

The problem seems to be that the offset of the currsize field is not correctly computed when accessed in 
add_to_set. This was fixed on the trunk as part of the fix for bug 227. However, this is not the same 
problem, so I will not mark it as a duplicate but rather resolve it as FIXED.
Comment 5 Gerd Behrmann 2005-12-05 09:46:29 CET
Correction: It was the fix of bug 229, that corrected this problem (bug 227 was fixed before the release of 
alpha 2).