// Represents a model of a pressure sensor.
class PressureSensor : Component
{
  // The pressure level that the sensor reports.
  private readonly int _pressure;

  // A persistent fault that can occur nondeterminisitcally; once it has occurred,
  // it cannot disappear.
  private readonly Fault _noPressureFault = new PermanentFault();

  // Instantiates an instance of a pressure sensor. The maximum allowed pressure is
  // passed in as a constructor argument, allowing for easy configuration and
  // re-use of component models.
  public PressureSensor(int pressure)
  {
      _pressure = pressure;
  }

  // Required port. This is the port that the sensor uses to sense the actual
  // pressure level in some environment component.
  public extern int CheckPhysicalPressure();

  // Provided port. Indicates whether the pressure level that the sensor is
  // configured to report has been reached.
  public virtual bool HasPressureLevelBeenReached()
  {
      return CheckPhysicalPressure() >= _pressure;
  }

  // Represents the effect of the fault '_noPressureFault'.
  [FaultEffect(Fault = nameof(_noPressureFault)]
  class SenseNoPressure : PressureTank
  {
      // Overwrites the behavior of the sensor's provided port, always returning the
      // constant 'false' when the fault is activated.
      public override bool HasPressureLevelBeenReached()
      {
          return false;
      }
  }
}

var result = SafetyAnalysis.AnalyzeHazard(model, hazard);

result.SaveCounterExamples("counter examples");
Console.WriteLine(result);