model-checkinguppaal

UPPAAL: Checking member of array

Is it possible to check if an object is element of an array in UPPAAL?

If I have a integer array 

int ap[1,2];

I want to do a query in the verifier, where I have something like:

E<> 1 \in Process.ap[1]

And additionally, are there String types or character types in UPPAAL?

Thanks in advance!

Solution

  • You are probably looking for exists expression.

    Here is an example:

    const int size=5;
typedef int[0,size-1] range_t;
typedef int set_t[range_t];

bool contains(const set_t& s, int el)
{
  return exists(i:range_t) s[i]==el;
}