Java Temperature Control System with Invariant Checks

Posted on Sep 24, 2025 in Computers

Java Temperature Control System Implementation

This document presents the implementation of a Java-based temperature control system, featuring an IncubatorController class with robust invariant checking using the VDM (Vienna Development Method) approach. It includes supporting classes for signals, custom exceptions, and a basic console-based tester.

Signal Class: Defining Temperature Change States

The Signal class acts as an enumeration for the possible actions related to temperature adjustment: increasing, decreasing, or doing nothing. It’s implemented as a class with static final instances, ensuring type safety and clear state representation.

public class Signal {
    private int value;

    public static final Signal INCREASE = new Signal(0);
    public static final Signal DECREASE = new Signal(1);
    public static final Signal DO_NOTHING = new Signal(2);

    private Signal(int x) {
        this.value = x;
    }

    @Override
    public boolean equals(Object obj) {
        if (this == obj) return true;
        if (obj == null || getClass() != obj.getClass()) return false;
        Signal signal = (Signal) obj;
        return value == signal.value;
    }

    @Override
    public String toString() {
        switch (value) {
            case 0: return "INCREASE";
            case 1: return "DECREASE";
            default: return "DO_NOTHING";
        }
    }
}

IncubatorController Class: Core Temperature Management

The IncubatorController class is responsible for managing the requested and actual temperatures within an incubator. It enforces strict preconditions and invariants to ensure the system operates within defined boundaries and maintains data integrity.

Constants and Attributes

• NIL: Represents an uninitialized or invalid temperature state.
• MAX: The maximum allowable temperature.
• MIN: The minimum allowable temperature.
• requestedTemp: The target temperature set by the user.
• actualTemp: The current measured temperature.

public class IncubatorController implements InvariantCheck {
    public static final int NIL = -999;
    public static final int MAX = 10;
    public static final int MIN = -10;

    private int requestedTemp;
    private int actualTemp;

Constructor

Initializes the controller with default NIL temperatures and performs an initial invariant check.

    public IncubatorController() {
        this.requestedTemp = NIL;
        this.actualTemp = NIL;
        VDM.invTest(this);
    }

Helper Method: inRange

A private utility method to check if a given temperature value falls within the allowed MIN and MAX range.

    private boolean inRange(int val) {
        return (MIN <= val && val <= MAX);
    }

Invariant Check Method: inv

This method defines the invariant for the IncubatorController. It ensures that both requestedTemp and actualTemp are either within the valid range or set to NIL.

    @Override
    public boolean inv() {
        return (inRange(requestedTemp) || requestedTemp == NIL) &&
               (inRange(actualTemp) || actualTemp == NIL);
    }

Public Methods for Temperature Control

• setInitialTemp(int tempIn)

  Sets the initial actual temperature. Throws a VDMException if the temperature is out of range or if actualTemp is not NIL (meaning it’s already been set).

      public void setInitialTemp(int tempIn) {
          if (!inRange(tempIn) || actualTemp != NIL) {
              throw new VDMException("Precondition violation for setInitialTemp");
          }
          actualTemp = tempIn;
          VDM.invTest(this);
      }

• requestChange(int tempIn)

  Sets the requested temperature and determines the initial Signal needed. Throws a VDMException if the temperature is out of range or if actualTemp is NIL (meaning it hasn’t been initialized).

      public Signal requestChange(int tempIn) {
          if (!inRange(tempIn) || actualTemp == NIL) {
              throw new VDMException("Precondition violation for requestChange");
          }
          requestedTemp = tempIn;
          Signal signalOut;
          if (tempIn > actualTemp) {
              signalOut = Signal.INCREASE;
          } else if (tempIn < actualTemp) {
              signalOut = Signal.DECREASE;
          } else {
              signalOut = Signal.DO_NOTHING;
          }
          VDM.invTest(this);
          return signalOut;
      }

• increment()

  Increases the actualTemp by one. Throws a VDMException if actualTemp is already greater than or equal to requestedTemp, or if either temperature is NIL.

      public Signal increment() {
          if (actualTemp >= requestedTemp || actualTemp == NIL || requestedTemp == NIL) {
              throw new VDMException("Precondition violation for increment");
          }
          actualTemp++;
          Signal signalOut = (actualTemp < requestedTemp) ? Signal.INCREASE :
                             Signal.DO_NOTHING;
          VDM.invTest(this);
          return signalOut;
      }

• decrement()

  Decreases the actualTemp by one. Throws a VDMException if actualTemp is already less than or equal to requestedTemp, or if either temperature is NIL.

      public Signal decrement() {
          if (actualTemp <= requestedTemp || actualTemp == NIL || requestedTemp == NIL) {
              throw new VDMException("Precondition violation for decrement");
          }
          actualTemp--;
          Signal signalOut = (actualTemp > requestedTemp) ? Signal.DECREASE :
                             Signal.DO_NOTHING;
          VDM.invTest(this);
          return signalOut;
      }

Getter Methods

Methods to retrieve the current requested and actual temperatures.

    public int getRequestedTemp() {
        return requestedTemp;
    }

    public int getActualTemp() {
        return actualTemp;
    }
}

VDM Support Classes and Interface

These classes provide the infrastructure for invariant checking based on the VDM principles.

VDMException Class

A custom runtime exception used to signal precondition or invariant violations within the system.

public class VDMException extends RuntimeException {
    public VDMException(String message) {
        super(message);
    }
}

VDM Class

A utility class containing a static method to test invariants. If an invariant is violated, it throws a VDMException.

public class VDM {
    public static void invTest(InvariantCheck obj) {
        if (!obj.inv()) {
            throw new VDMException("Invariant violation");
        }
    }
}

InvariantCheck Interface

An interface that classes must implement to provide an invariant checking method.

public interface InvariantCheck {
    boolean inv();
}

IncubatorControllerTester Class: System Demonstration

This class provides a simple console-based application to interact with and test the IncubatorController. It demonstrates how to use the controller’s methods and handles VDMExceptions gracefully. Note: This tester assumes the existence of an EasyIn utility class for console input.

public class IncubatorControllerTester {

    public static void main(String[] args) {
        IncubatorController controller;
        try {
            controller = new IncubatorController();
        } catch (VDMException e) {
            System.out.println("Error: Initial object violates invariant.");
            e.printStackTrace();
            return;
        }

        char choice;
        do {
            System.out.println("\n--- IncubatorController Tester ---");
            System.out.println("1. Display temperatures");
            System.out.println("2. Set initial temperature");
            System.out.println("3. Request temperature change");
            System.out.println("4. Increment temperature");
            System.out.println("5. Decrement temperature");
            System.out.println("6. Quit");
            System.out.print("Enter choice (1-6): ");
            choice = EasyIn.getchar();

            try {
                switch (choice) {
                    case '1': opt1(controller); break;
                    case '2': opt2(controller); break;
                    case '3': opt3(controller); break;
                    case '4': opt4(controller); break;
                    case '5': opt5(controller); break;
                    case '6': opt6("Exiting tester..."); break;
                    default: System.out.println("Invalid choice. Please select 1-6.");
                }
            } catch (VDMException e) {
                System.out.println("Error: " + e.getMessage());
            }
        } while (choice != '6');
    }

    public static void opt1(IncubatorController controller) {
        System.out.println("Requested Temperature: " + controller.getRequestedTemp());
        System.out.println("Actual Temperature: " + controller.getActualTemp());
    }

    public static void opt2(IncubatorController controller) {
        System.out.print("Enter initial temperature: ");
        int temp = EasyIn.getInt();
        controller.setInitialTemp(temp);
        System.out.println("Initial temperature set.");
    }

    public static void opt3(IncubatorController controller) {
        System.out.print("Enter requested temperature: ");
        int temp = EasyIn.getInt();
        Signal signal = controller.requestChange(temp);
        System.out.println("Requested temperature set. Signal: " + signal);
    }

    public static void opt4(IncubatorController controller) {
        Signal signal = controller.increment();
        System.out.println("Temperature incremented. Signal: " + signal);
    }

    public static void opt5(IncubatorController controller) {
        Signal signal = controller.decrement();
        System.out.println("Temperature decremented. Signal: " + signal);
    }

    public static void opt6(String message) {
        System.out.println(message);
    }
}