/**************************************************************
* Sample model to estimate the state of a database table
* author: Marius Mikucionis marius@cs.aau.dk
*/
const int MAXIND=3; // max size of index domain
const int MAXVAL=2; // max size of data domain
const int MAXLEN=MAXIND*(MAXVAL+1); // max size of database table
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;
const tuple_t tuple_zero = { 0, 0 };
const bool beataroundabush=false;//disables non-interesting transitions
bool overflow;// is set upon overflow in the list
// global variable to communicate tuples with iut:
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 :-(
// finds an element and returns its index or -1 if not found
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;
}
// checks whether the elements belongs to set
bool isMember(const tuple_t set[MAXLEN], const tuple_t v) {
return (getIndex(set, v)>=0);
}
// alllocates a space
void shiftToRight(int[0,MAXLEN] from, tuple_t &set[MAXLEN]){
int i;
if (set[MAXLEN-1].id>0) overflow = true;
for (i=MAXLEN-1; i>from; --i) set[i]=set[i-1];
}
// deallocates
void shiftToLeft(int[0,MAXLEN] from, tuple_t &set[MAXLEN]){
int i;
for (i=from; i<MAXLEN-1; ++i) set[i]=set[i+1];
set[MAXLEN-1] = tuple_zero; // cleanup last element
}
void addToSet(tuple_t &set[MAXLEN], const tuple_t &v){
int i;
if (isMember(set, v)) return;
// list should be sorted descending by id
// find empty or less element:
for (i=0; i<MAXLEN and v.id<set[i].id; ++i);
for (i=i; i<MAXLEN and v.id==set[i].id and v.data<=set[i].data; ++i);
if (i<MAXLEN) {
if (set[i].id>0) shiftToRight(i, set);// make more space
set[i]=v; // fill it with new member
} else overflow = true;
}
void remFromSet(tuple_t &set[MAXLEN], const tuple_t &v){
int i = getIndex(set, v); // try to find it
if (i>=0) {// found it
shiftToLeft(i, set); // overwrite with next values
} // else v is not in the set, nothing to remove
}
// list to track the present tuples:
tuple_t present[MAXLEN]; // by default all id=0 (means empty list)
// list to track the absent tuples:
tuple_t absent[MAXLEN]; // by default all id=0 (means empty list)
// list for sample table in deterministic implementation:
tuple_t table[MAXLEN]={
{2,2}, {1,1},
{0,0},{0,0},{0,0},{0,0},{0,0},
{0,0},{0,0}/*,{0,0},{0,0},{0,0}/*,
{0,0},{0,0},{0,0},{0,0},{0,0},
{0,0},{0,0},{0,0},{0,0},{0,0},
{0,0},{0,0},{0,0},{0,0},{0,0},
{0,0},{0,0},{0,0}*/
};testerupdate2update1callgenerateimplementationconst tuple_t one = {1, 1};
const tuple_t two = {2, 2};
void initialize(){
addToSet(table, one);
addToSet(table, two);
}initialrespond2respond1waitsystem tester, implementation;