Preamble
Programmable thermostat is a software case study (see also here … in French),
which is implemented in State Chart XML 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
JavaFX application as a Maven project
Programmable_thermostat_JavaFX.PauWare2Web.zip
Installation requirements
This application has been designed and tested by means of PauWare ver. 2.0 (a.k.a. PauWare2 , Sept. 2021).
This application also reuses PauWare2Web , a PauWare2 add-on, which allows the dynamic simulation of Harel's Statecharts in a Web browser.
While PauWare2 is based on Java 9,
PauWare2Web requires Java 11 .
After downloading
Programmable_thermostat_JavaFX.PauWare2Web.zip
PauWare2
PauWare2.zip PauWare2Web
PauWare2Web.zip Maven dependencies.
PauWare2Web itself requires third-party libraries that are downloaded by Maven :
Java API for Processing JSON software is linked to PauWare2Web as a runtime library.
PlantUML Java software is linked to PauWare2Web as a runtime library.
Graphviz software (required by PlantUML ) is a priori installed on Windows .
Graphviz software on macOS may be installed using Homebrew
(see also here …).
Tyrus Java software is linked to PauWare2Web as a runtime library.
Specification (statechart) as full-size SVG image
Programmable_thermostat entry/ Programmable_thermostat.to_be_set(Long) exit/ Programmable_thermostat.to_be_killed Control allow: fan_switch_turned_on/Fan_relay.run allow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_greaterThan_target_temperature]/Air_conditioner_relay.run allow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_greaterThan_target_temperature]/Fan_relay.run allow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_greaterThan_target_temperature]/Run_indicator.on allow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_greaterThan_target_temperature_plus_delta]/Furnace_relay.stop allow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_greaterThan_target_temperature_plus_delta]/Run_indicator.off allow: 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.run allow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_lessThan_target_temperature]/Fan_relay.run allow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_lessThan_target_temperature]/Run_indicator.on allow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_lessThan_target_temperature_minus_delta]/Air_conditioner_relay.stop allow: ambient_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_lessThan_target_temperature_minus_delta]/Run_indicator.off allow: 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.run allow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_greaterThan_target_temperature]/Fan_relay.run allow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_greaterThan_target_temperature]/Run_indicator.on allow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_greaterThan_target_temperature_plus_delta]/Furnace_relay.stop allow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_greaterThan_target_temperature_plus_delta]/Run_indicator.off allow: 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.run allow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_lessThan_target_temperature]/Fan_relay.run allow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_heat_and_ambient_temperature_lessThan_target_temperature]/Run_indicator.on allow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_lessThan_target_temperature_minus_delta]/Air_conditioner_relay.stop allow: target_temperature_changed[Programmable_thermostat.season_switch_in_Is_cool_and_ambient_temperature_lessThan_target_temperature_minus_delta]/Run_indicator.off allow: 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.stop allow: season_switch_turned_off/Furnace_relay.stop allow: season_switch_turned_off/Run_indicator.off allow: season_switch_turned_off/Fan_relay.stop(Boolean) Setup_Operate Setup allow: time_out[Programmable_thermostat.no_input_lessThan_ninety]/Programmable_thermostat.set_no_input(Integer) Programmable_thermostat→ Programmable_thermostat→ Current_date_and_time_refreshing entry/ Programmable_thermostat.display_current_date_and_time Program_refreshing Program_target_temperature_refreshing allow: temp_down/Programmable_thermostat.set_no_input(Integer) allow: temp_up/Programmable_thermostat.set_no_input(Integer) entry/ Programmable_thermostat.display_program_target_temperature f_c/Programmable_thermostat.switch_mode Period_and_program_time_refreshing entry/ Programmable_thermostat.display_period_and_program_time time_backward/Programmable_thermostat.set_no_input(Integer) time_forward/Programmable_thermostat.set_no_input(Integer) set_clock set_day/Programmable_thermostat.set_no_input(Integer) time_backward time_forward view_program/Programmable_thermostat.set_no_input(Integer) Set_time Programmable_thermostat→ Set_current_minute allow: time_backward/Programmable_thermostat.set_time(Integer) allow: time_forward/Programmable_thermostat.set_time(Integer) Set_current_hour allow: time_backward/Programmable_thermostat.set_time(Integer) allow: time_forward/Programmable_thermostat.set_time(Integer) Programmable_thermostat→ Programmable_thermostat→ Set_program Set_program_target_temperature allow: temp_down[Programmable_thermostat.program_period_target_temperature_greaterThan_Min]/Temperature.decrement allow: temp_up[Programmable_thermostat.program_period_target_temperature_lessThan_Max]/Temperature.increment Set_program_time allow: time_backward/Programmable_thermostat.set_program_time(Integer) allow: time_forward/Programmable_thermostat.set_program_time(Integer) Set_period allow: 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_day allow: 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_day Operate Target_temperature_displaying entry/ Programmable_thermostat.display_target_temperature temp_down[Programmable_thermostat.target_temperature_greaterThan_Min]/^Programmable_thermostat.target_temperature_changed temp_up[Programmable_thermostat.target_temperature_lessThan_Max]/^Programmable_thermostat.target_temperature_changed f_c/Programmable_thermostat.switch_mode Ambient_temperature_displaying_Current_date_and_time_displaying Programmable_thermostat→ Ambient_temperature_displaying entry/ Programmable_thermostat.display_ambient_temperature Current_date_and_time_displaying entry/ Programmable_thermostat.display_current_date_and_time run_program time_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_c time_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_Hold Programmable_thermostat→ Run allow: temp_down[Programmable_thermostat.target_temperature_greaterThan_Min]/Temperature.decrement allow: temp_up[Programmable_thermostat.target_temperature_lessThan_Max]/Temperature.increment allow: time_out[Programmable_thermostat.not_weekend]/Programmable_thermostat.set_target_temperature(Integer,Integer) allow: time_out[Programmable_thermostat.not_weekend]/Programmable_thermostat.display_target_temperature allow: time_out[Programmable_thermostat.weekend]/Programmable_thermostat.set_target_temperature(Integer,Integer) allow: time_out[Programmable_thermostat.weekend]/Programmable_thermostat.display_target_temperature Hold allow: temp_down[Programmable_thermostat.target_temperature_greaterThan_Min]/Temperature.decrement allow: temp_up[Programmable_thermostat.target_temperature_lessThan_Max]/Temperature.increment run_program hold_temp time_out[Programmable_thermostat.no_input_greaterThan_or_equal_to_ninety] 
