const int MAXLEN=10; // max size of database table
const int MAXIND=10; // max size of index domain
const int MAXVAL=10; // max size of value domain
typedef int[0,MAXIND] id_t; // the id type
typedef int[0,MAXIND] data_t; // the data type
typedef struct {
id_t id; // 1..MAXIND are good, id=0 means empty
data_t data;// 0..MAXVAL are possible data values
// add more atributes if needed...
} tuple_t;
tuple_t value;
chan addValue, remValue;
chan success, failed;
// references make Uppaal think that functions are not side-effect-free
// hence, reference args cannot be used in guards...
// this needs to be fixed in UTAP typechecker :-(
int getIndex(const tuple_t set[MAXLEN], const tuple_t v) {
int i;
for (i=0; i<MAXLEN; ++i) // iterate through entire array
if (v.id == set[i].id and v.data == set[i].data) return i;
return -1;
}
bool isMember(const tuple_t set[MAXLEN], const tuple_t v) {
return (getIndex(set, v)>=0);
}
void addToSet(tuple_t &set[MAXLEN], tuple_t &v){
int i;
for (i=0; i<MAXLEN and set[i].id!=0; ++i) // find empty place
if (i<MAXLEN) // found empty
set[i]=v; // fill it with new member
// else ran out of space in the list :-(
}
void remFromSet(tuple_t &set[MAXLEN], tuple_t &v){
int i = getIndex(set, v); // try to find it
if (i>=0) {// found it
set[i].id=0; // remove
set[i].data=0; // cleanup to preserve state space
} // else error: v is not in the set
}
bool equalSets(const tuple_t set1[MAXLEN], const tuple_t set2[MAXLEN]) {
// this is not precise, need to examine member by member...
int i;
for (i=0; i<MAXLEN; ++i)
if (set1[i].id != set2[i].id or set1[i].data != set2[i].data)
return false;
return true;
}
testertuple_t present[MAXLEN]; // by default all id=0 (means empty list)
tuple_t absent[MAXLEN]; // by default all id=0 (means empty list)
update2update1callgenerateimplementationtuple_t table[MAXLEN] = {
{1, 1}, {2, 2}, {3, 3}, {4, 4}, {5, 5}, // first half filled
{0, 0}, {0, 0}, {0, 0}, {0, 0}, {0, 0} // second empty
};
system tester, implementation;