12. Examples¶
12.1. The Water Sprinkler¶
class WaterSprinkler {
boolean cloudy {
[ 0.5, // false
0.5] // true
};
boolean sprinkler dependson cloudy {
// false, true => cloudy
[ 0.5, 0.9, // sprinkler == false
0.5, 0.1] // sprinkler == true
};
boolean rain dependson cloudy {
// false, true => cloudy
[ 0.8, 0.2, // rain == false
0.2, 0.8] // rain == true
};
boolean wet_grass dependson rain, sprinkler {
// wet_grass
// rain, sprinkler| false, true
*, *: 0.1, 0.9;
false, false: 1.00, 0.00;
true, true: 0.01, 0.99;
};
}
system MyFirstSystem {
WaterSprinkler water_sprinkler;
}
12.2. The Printer Example¶
type t_state labels (OK, NOK);
class PowerSupply {
t_state powState {
[0.99, // OK
0.01] // NOK
};
}
class Room {
PowerSupply power;
}
class Printer {
Room room;
boolean hasPaper {
[ 0.1, // false
0.9 ] // true
};
boolean hasInk {
[ 0.3, // false
0.7 ] // true
};
t_state equipState dependson
room.power.powState, hasPaper, hasInk { // OK, NOK
*, *, *: 0.00, 1.00;
OK, true, true: 0.80, 0.20;
};
}
class Computer {
Room room;
Printer[] printers;
boolean exists_printer = exists ( [printers.equipState], OK );
boolean can_print = and([printers.equipState, exists_printer]);
}
12.3. Printers with inheritance¶
type t_state extends boolean (
OK: true,
NOK: false
);
type t_ink extends t_state (
NotEmpty: OK,
Empty: NOK
);
type t_paper extends t_state (
Ready: OK,
Jammed: NOK,
Empty: NOK);
class PowerSupply {
t_state state {
["0.99", // OK
"0.01"] // NOK
};
}
class Room {
PowerSupply power;
}
interface Printer {
Room room;
t_state equipState;
boolean hasPaper;
boolean hasInk;
}
class BWPrinter implements Printer {
Room room;
t_ink hasInk {
[0.8, // NotEmpty
0.2] // Empty
};
t_paper hasPaper {
[0.7, // Ready
0.2, // Jammed
0.1] // Empty
};
t_state equipState dependson room.power.state, hasInk, hasPaper {
// OK, NOK
*, *, *: 0.0, 1.0;
OK, NotEmpty, Ready: 1.0, 0.0;
};
}
class ColorPrinter implements Printer {
Room room;
t_ink black {
[0.8, // NotEmpty
0.2] // Empty
};
t_ink magenta {
[0.8, // NotEmpty
0.2] // Empty
};
t_ink yellow {
[0.8, // NotEmpty
0.2] // Empty
};
t_ink cyan {
[0.8, // NotEmpty
0.2] // Empty
};
boolean hasInk = forall ( [black, magenta, yellow, cyan], NotEmpty );
t_paper hasPaper {
[0.7, // Ready
0.2, // Jammed
0.1] // Empty
};
t_state equipState dependson room.power.state, hasPaper, hasInk, black {
// OK, NOK
*, *, *, *: 0.00, 1.00;
*, *, false, NotEmpty: 0.00, 0.00;
OK, Ready, true, *: 0.99, 0.01;
};
}
class Computer {
Room room;
Printer[] printers;
boolean functional_printer = exists ( printers.equipState, OK );
boolean degraded_printer = exists ( printers.equipState, Degraded );
boolean working_printer = exists ( [functional_printer, degraded_printer], true );
t_state equipState dependson room.power.state {
// OK, NOK
OK: 0.90, 0.10;
NOK: 0.00, 1.00;
};
boolean can_print = and([working_printer, (boolean)equipState]);
}