Programmable thermostat

Preamble

Programmable thermostat is a software case study (see also here… in French), which is implemented in State Chart XML (SCXML) and PauWare. PauWare is a Java engine for executing Harel's Statecharts in general.

Application Programming Interface (API): Javadoc.

Goal

This case study aims at illustrating the advanced use of PauWare, i.e., while the “true” JavaFX app. is running, the Web browser animates models at run-time according to events occurring in the real app.

Resources
Installation requirements
Specification (statechart) as full-size SVG image
Programmable_thermostatentry/ Programmable_thermostat.to_be_set(Long)exit/ Programmable_thermostat.to_be_killedControlallow: fan_switch_turned_on/Fan_relay.runallow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_greaterThan_target_temperature]/Air_conditioner_relay.runallow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_greaterThan_target_temperature]/Fan_relay.runallow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_greaterThan_target_temperature]/Run_indicator.onallow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_greaterThan_target_temperature_plus_delta]/Furnace_relay.stopallow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_greaterThan_target_temperature_plus_delta]/Run_indicator.offallow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_greaterThan_target_temperature_plus_delta]/Fan_relay.stop(Boolean)allow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_lessThan_target_temperature]/Furnace_relay.runallow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_lessThan_target_temperature]/Fan_relay.runallow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_lessThan_target_temperature]/Run_indicator.onallow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_lessThan_target_temperature_minus_delta]/Air_conditioner_relay.stopallow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_lessThan_target_temperature_minus_delta]/Run_indicator.offallow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_lessThan_target_temperature_minus_delta]/Fan_relay.stop(Boolean)allow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_greaterThan_target_temperature]/Air_conditioner_relay.runallow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_greaterThan_target_temperature]/Fan_relay.runallow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_greaterThan_target_temperature]/Run_indicator.onallow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_greaterThan_target_temperature_plus_delta]/Furnace_relay.stopallow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_greaterThan_target_temperature_plus_delta]/Run_indicator.offallow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_greaterThan_target_temperature_plus_delta]/Fan_relay.stop(Boolean)allow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_lessThan_target_temperature]/Furnace_relay.runallow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_lessThan_target_temperature]/Fan_relay.runallow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_lessThan_target_temperature]/Run_indicator.onallow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_lessThan_target_temperature_minus_delta]/Air_conditioner_relay.stopallow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_lessThan_target_temperature_minus_delta]/Run_indicator.offallow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_lessThan_target_temperature_minus_delta]/Fan_relay.stop(Boolean)allow: season_switch_turned_off/Air_conditioner_relay.stopallow: season_switch_turned_off/Furnace_relay.stopallow: season_switch_turned_off/Run_indicator.offallow: season_switch_turned_off/Fan_relay.stop(Boolean)Setup_OperateSetupallow: time_out[Programmable_thermostat.no_input_lessThan_ninety]/Programmable_thermostat.set_no_input(Integer)Programmable_thermostat→Programmable_thermostat→Current_date_and_time_refreshingentry/ Programmable_thermostat.display_current_date_and_timeProgram_refreshingProgram_target_temperature_refreshingallow: temp_down/Programmable_thermostat.set_no_input(Integer)allow: temp_up/Programmable_thermostat.set_no_input(Integer)entry/ Programmable_thermostat.display_program_target_temperaturef_c/Programmable_thermostat.switch_modePeriod_and_program_time_refreshingentry/ Programmable_thermostat.display_period_and_program_timetime_backward/Programmable_thermostat.set_no_input(Integer)time_forward/Programmable_thermostat.set_no_input(Integer)set_clockset_day/Programmable_thermostat.set_no_input(Integer)time_backwardtime_forwardview_program/Programmable_thermostat.set_no_input(Integer)Set_timeProgrammable_thermostat→Set_current_minuteallow: time_backward/Programmable_thermostat.set_time(Integer)allow: time_forward/Programmable_thermostat.set_time(Integer)Set_current_hourallow: time_backward/Programmable_thermostat.set_time(Integer)allow: time_forward/Programmable_thermostat.set_time(Integer)Programmable_thermostat→Programmable_thermostat→Set_programSet_program_target_temperatureallow: temp_down[Programmable_thermostat.program_period_target_temperature_greaterThan_Min]/Temperature.decrementallow: temp_up[Programmable_thermostat.program_period_target_temperature_lessThan_Max]/Temperature.incrementSet_program_timeallow: time_backward/Programmable_thermostat.set_program_time(Integer)allow: time_forward/Programmable_thermostat.set_program_time(Integer)Set_periodallow: view_program[Programmable_thermostat.period_equal_to_eight]/Programmable_thermostat.set_period(Integer)allow: view_program[Programmable_thermostat.period_not_equal_to_eight]/Programmable_thermostat.set_period(Integer)Set_current_dayallow: time_backward/Programmable_thermostat.set_time(Integer)allow: time_forward/Programmable_thermostat.set_time(Integer)view_program/Programmable_thermostat.set_period(Integer)set_clock/Programmable_thermostat.set_no_input(Integer)set_clock/Programmable_thermostat.set_no_input(Integer)set_dayOperateTarget_temperature_displayingentry/ Programmable_thermostat.display_target_temperaturetemp_down[Programmable_thermostat.target_temperature_greaterThan_Min]/^Programmable_thermostat.target_temperature_changedtemp_up[Programmable_thermostat.target_temperature_lessThan_Max]/^Programmable_thermostat.target_temperature_changedf_c/Programmable_thermostat.switch_modeAmbient_temperature_displaying_Current_date_and_time_displayingProgrammable_thermostat→Ambient_temperature_displayingentry/ Programmable_thermostat.display_ambient_temperatureCurrent_date_and_time_displayingentry/ Programmable_thermostat.display_current_date_and_timerun_programtime_out[Programmable_thermostat.alternately_equal_to_two]/Programmable_thermostat.set_alternately(Integer);Programmable_thermostat.set_time(Integer)time_out[Programmable_thermostat.alternately_equal_to_two]/Programmable_thermostat.set_alternately(Integer);Programmable_thermostat.set_time(Integer)f_ctime_out[Programmable_thermostat.alternately_not_equal_to_two]/Programmable_thermostat.set_alternately(Integer);Programmable_thermostat.set_time(Integer)time_out[Programmable_thermostat.alternately_not_equal_to_two]/Programmable_thermostat.set_alternately(Integer);Programmable_thermostat.set_time(Integer)Run_HoldProgrammable_thermostat→Runallow: temp_down[Programmable_thermostat.target_temperature_greaterThan_Min]/Temperature.decrementallow: temp_up[Programmable_thermostat.target_temperature_lessThan_Max]/Temperature.incrementallow: time_out[Programmable_thermostat.not_weekend]/Programmable_thermostat.set_target_temperature(Integer,Integer)allow: time_out[Programmable_thermostat.not_weekend]/Programmable_thermostat.display_target_temperatureallow: time_out[Programmable_thermostat.weekend]/Programmable_thermostat.set_target_temperature(Integer,Integer)allow: time_out[Programmable_thermostat.weekend]/Programmable_thermostat.display_target_temperatureHoldallow: temp_down[Programmable_thermostat.target_temperature_greaterThan_Min]/Temperature.decrementallow: temp_up[Programmable_thermostat.target_temperature_lessThan_Max]/Temperature.incrementrun_programhold_temptime_out[Programmable_thermostat.no_input_greaterThan_or_equal_to_ninety]