Petra Example (with symbolic semantics)

Example: Light System (with symbolic semantics)

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().toggle(); // [toggle] = [toggle_0] ∪ [toggle_1] = {off->on} ∪ {on->off} = {off->on, on->off}
    }
}

Light (entry point)

// [Light] = [Power] X [Control] = {on,off} X {on,off}
public final class Light {
    private final Power power = new Power(); // [Power] = {on,off}
    private final Control control = new Control(); // [Control] = {on,off}

    @Initial
    public boolean off() { return power.on() && control.off(); } // [off] = {(p,c) ∈ Power X Control | p=on & c=off } = {(on,off)}
    public boolean on() { return power.on() && control.on(); } // [on] = {(p,c) ∈ Power X Control | p=on & c=on } =  {(on,on)}

    // [toggle] = [toggle_0] ∪ [toggle_1] = {off->on} ∪ {on->off} = {off->on, on->off}
    public void toggle() {
        // [toggle_0] = {off->on} if [control.turnOn]([off]) ⊆ [on]
        if (off()){ // [off] = {(p,c) ∈ [Power] X [Control] | p=on & c=off } = {(on,off)}
            control.turnOn(); // [control.turnOn] = {on->on, off->off} X {on->on, off->on} = {(on,on)->(on,on), (on,off)->(on,on), (off,on)->(off,on), (off,off)->(off,on)}
            assert(on()); // [on] = {(p,c) ∈ [Power] X [Control] | p=on & c=on } = {(on,on)}
        } else
        // [toggle_1] = {on->off} if [control.turnOff]([on]) ⊆ [off]
        if (on()){ // [on] = {(p,c) ∈ [Power] X [Control] | p=on & c=on } = {(on,on)}
            control.turnOff(); // [control.turnOff] = {on->on, off->off} X {on->off, off->off} = {(on,on)->(on,off), (on,off)->(on,off), (off,on)->(off,off), (off,off)->(off,off)}
            assert(off()); // [off] = {(p,c) ∈ [Power] X [Control] |  p=on & c=off } = {(on,off)}
        }
    }
}

Power

 // [Power] = {on,off}
@Base public final class Power {
  private boolean bool = true;

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

  public void turnOn() { // [turnOn] = {on,off} -> {on} = {on->on, off->on}
    if (on() || off()){ // [on] ∪ [off] = {on} ∪ {off} = {on,off}
      bool=true;
      assert(on()); // [on] = {on}
    }
  }

  public void turnOff() { // [turnOff] = {on,off} -> {off} = {on->off, off->off}
    if (on() || off()){ // [on] ∪ [off] = {on} ∪ {off} = {on,off}
      bool=false;
      assert(off()); // [off] = {off}
    }
  }
}

Control

// [Control] = {on,off}
@Base public final class Control {
  private boolean bool = false;

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

  public void turnOn() { // [turnOn] = {on,off} -> {on} = {on->on, off->on}
      if (on() || off()){ // {on} ∪ {off} = {on,off}
          bool=true;
          assert(on()); // {on}
      }
  }

  public void turnOff() { // [turnOff] = {on,off} -> {off} = {on->off, off->off}
      if (on() || off()){ // {on} ∪ {off} = {on,off}
          bool=false;
          assert(off()); // {off}
      }
  }
}