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

Bug 234

Summary: Problem with verifyta
Product: UPPAAL Reporter: Venkita Subramonian <venkita>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: RESOLVED FIXED    
Severity: blocker    
Priority: P1    
Version: 3.6 Alpha 2   
Hardware: PC   
OS: Linux   
Architecture:
Attachments: Test case (XML)

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