Petra Example

Example: Light System

Main

This is used to start a Petra system.

import static com.cognitionbox.petra.ast.interp.util.Program.start;

public class Main {
    public static void main(String[] args){
        new Light().run();
    }
}

Light (entry point)

public final class Light {
  private final Power power = new Power();
  private final Control control = new Control();

  @Initial
  public boolean off() { return power.on() && control.off(); }
  public boolean on() { return power.on() && control.on(); }

  public void toggle() {
    if (off()){
      control.turnOn();
      assert(on());
    } else if (on()){
      control.turnOff();
      assert(off());
    }
  }
}

Power

@Base public final class Power {
  private boolean bool = true;

  public boolean off() { return bool==false; }
  @Initial
  public boolean on() { return bool==true; }

  public void turnOn() {
    if (on() || off()){
      bool=true;
      assert(on());
    }
  }

  public void turnOff() {
    if (on() || off()){
      bool=false;
      assert(off());
    }
  }
}

Control

@Base public final class Control {
  private boolean bool = false;

  @Initial
  public boolean off() { return bool==false; }
  public boolean on() { return bool==true; }

  public void turnOn() {
    if (on() || off()){
      bool=true;
      assert(on());
    }
  }

  public void turnOff() {
    if (on() || off()){
      bool=false;
      assert(off());
    }
  }
}