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]);
}