diff --git a/isolette/readme.md b/isolette/readme.md index 2ae8679..bc3b924 100644 --- a/isolette/readme.md +++ b/isolette/readme.md @@ -17,7 +17,7 @@ cd INSPECTA-models ``` -1. Clone the SysMLv2 AADL Libraries into the Isolette sysml directory +1. Clone the [SysMLv2 AADL Libraries](https://github.com/santoslab/sysml-aadl-libraries.git) into the Isolette sysml directory ``` git clone https://github.com/santoslab/sysml-aadl-libraries.git isolette/sysml/sysml-aadl-libraries @@ -81,7 +81,9 @@ - [microkit #175](https://github.com/seL4/microkit/pull/175) - [seL4 #1308](https://github.com/seL4/seL4/pull/1308) -## JVM +## Codegen + +### JVM 1. *OPTIONAL* Rerun codegen targeting the JVM @@ -119,7 +121,7 @@ sireum hamr sysml logika --sourcepath isolette/sysml ``` -## Microkit +### Microkit 1. *OPTIONAL* Rerun codegen targeting Microkit @@ -152,6 +154,7 @@ Type ``CTRL-a x`` to exit the QEMU simulation + You should see output similar to the following ``` Booting all finished, dropped to user space diff --git a/isolette/sysml/arch.png b/isolette/sysml/arch.png deleted file mode 100644 index 12609d9..0000000 Binary files a/isolette/sysml/arch.png and /dev/null differ diff --git a/isolette/sysml/arch.svg b/isolette/sysml/arch.svg index 6810215..e352004 100644 --- a/isolette/sysml/arch.svg +++ b/isolette/sysml/arch.svg @@ -1,27 +1,27 @@ -isolette.single_sensor*Isolette.Single_Sensor*air_temperatureoperator_commandsoperator_alarmoperator_visual_informationheat_outisolette_processor*heat_source*heat_controlheat_outcpi*heat_controlheat_outheat_controller*heat_controlheat_outoperator_interface*monitor_statusalarm_controldisplay_temperatureoperator_commandsregulator_statusoperator_visual_informationlower_desired_tempWstatusupper_desired_tempWstatusupper_alarm_tempWstatuslower_alarm_tempWstatusoperator_alarmoip*monitor_statusalarm_controldisplay_temperatureregulator_statuslower_desired_tempWstatusupper_desired_tempWstatusupper_alarm_tempWstatuslower_alarm_tempWstatusoit*monitor_statusalarm_controldisplay_temperatureregulator_statuslower_desired_tempWstatusupper_desired_tempWstatusupper_alarm_tempWstatuslower_alarm_tempWstatustemperature_sensor*aircurrent_tempWstatuscpi*aircurrent_tempWstatusthermostat*aircurrent_tempWstatusthermostatthermostat_single_sensor.implthermostat*lower_desired_tempWstatusupper_desired_tempWstatusupper_alarm_tempWstatuscurrent_tempWstatuslower_alarm_tempWstatusalarm_controlheat_controlmonitor_statusdisplay_temperatureregulator_statusmonitor_temperaturemt*Monitor::Monitor_Temperature.implcurrent_tempWstatusupper_alarm_tempWstatuslower_alarm_tempWstatusmonitor_statusalarm_controlmanage_monitor_mode*mmi*Monitor::Manage_Monitor_Mode.implcurrent_tempWstatusinterface_failureupper_alarm_tempWstatusinternal_failurelower_alarm_tempWstatuscurrent_tempWstatusmonitor_modemonitor_modeinterface_failuremanage_monitor_interface*monitor_statusMonitor::Manage_Monitor_Interface.implupper_alarm_templower_alarm_tempmmi*current_tempWstatusupper_alarm_tempWstatuslower_alarm_tempWstatusmonitor_modeinterface_failuremonitor_statusupper_alarm_templower_alarm_tempdmf*internal_failuredmf*internal_failurema*upper_alarm_tempcurrent_tempWstatuslower_alarm_tempmonitor_modemanage_alarm*alarm_controlMonitor::Manage_Alarm.implma*upper_alarm_tempcurrent_tempWstatuslower_alarm_tempmonitor_modealarm_controlmmm*interface_failuredetect_monitor_failure*internal_failurecurrent_tempWstatusmonitor_modemmm*interface_failureinternal_failurecurrent_tempWstatusmonitor_modert*lower_desired_tempWstatusupper_desired_tempWstatuscurrent_tempWstatusheat_controldisplayed_tempregulator_statusmrm*interface_failureinternal_failurecurrent_tempWstatusregulator_modemrm*interface_failureinternal_failurecurrent_tempWstatusregulator_modemri*lower_desired_tempWstatusregulate_temperature*upper_desired_tempWstatuslower_desired_tempWstatuscurrent_tempWstatusupper_desired_tempWstatusregulator_modecurrent_tempWstatuslower_desired_tempheat_controlinterface_failuredisplayed_tempupper_desired_tempregulator_statusdisplayed_tempmanage_regulator_interface*regulator_statusRegulate::Manage_Regulator_Interface.implmri*lower_desired_tempWstatusupper_desired_tempWstatuscurrent_tempWstatusregulator_modelower_desired_tempinterface_failureupper_desired_tempdisplayed_tempregulator_statusdetect_regulator_failure*mhs*internal_failurelower_desired_tempcurrent_tempWstatusmanage_heat_source*upper_desired_tempRegulate::Manage_Heat_Source.implregulator_modeheat_controlmhs*lower_desired_tempcurrent_tempWstatusupper_desired_tempregulator_modeheat_controlmanage_regulator_mode*drf*Regulate::Manage_Regulator_Mode.implinternal_failureinternal_failuredrf*current_tempWstatusinternal_failureinterface_failureregulator_mode