creating CabineTemperature theory
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Idir AIT SADOUNE 2022-07-21 09:38:51 +01:00
parent d049690120
commit 0e66068c7a
2 changed files with 30 additions and 15 deletions

View File

@ -203,19 +203,4 @@ doc_class PicturePushButton = Widget +
(* TO BE COMPLETED *)
invariant force_widget_type_8 :: "widget_type \<sigma> = A661_PICTURE_PUSH_BUTTON"
(* INSTANCES *)
text*[TemperatureCelciusScale::Picture, widget_ident=4642,parent_ident="Some 4641"]\<open>\<close>
text*[TemperatureIndicatedPointer::Symbol, widget_ident=4643,parent_ident="Some 4641"]\<open>\<close>
text*[TemperatureSelectedPointer::Symbol, widget_ident=4644,parent_ident="Some 4641"]\<open>\<close>
text*[IndicatedTempDRO::Label, widget_ident=4645,parent_ident="Some 4641", label_string="\<open>24\<close>"]\<open>\<close>
text*[IndicatedUnitLabel::Label, widget_ident=4645,parent_ident="Some 4641", label_string="\<open>C\<close>"]\<open>\<close>
text*[IncreaseSelectTemp::PicturePushButton, widget_ident=4646,parent_ident="Some 4641"]\<open>\<close>
text*[DecreaseSelectTemp::PicturePushButton, widget_ident=4647,parent_ident="Some 4641"]\<open>\<close>
text*[CabinTempPanel::Panel, widget_ident=4641]\<open>\<close>
text*[Layer66::Layer, layer_id=66, widgets_tree="{CabinTempPanel, DecreaseSelectTemp, IncreaseSelectTemp, IndicatedUnitLabel, IndicatedTempDRO, TemperatureSelectedPointer, TemperatureIndicatedPointer, TemperatureCelciusScale}"]\<open>\<close>
text*[CabineTemperature::Window, application_id="0x6788", contained_layers="{@{Layer \<open>Layer66\<close>}}"]\<open>\<close>
end

View File

@ -0,0 +1,30 @@
theory CabineTemperature
imports ARINC_661
begin
value*[TemperatureCelciusScale::Picture, widget_ident=4642,parent_ident="Some 4641"]
\<open>@{Picture \<open>TemperatureCelciusScale\<close>}\<close>
value*[TemperatureIndicatedPointer::Symbol, widget_ident=4643,parent_ident="Some 4641"]
\<open>@{Symbol \<open>TemperatureIndicatedPointer\<close>}\<close>
value*[TemperatureSelectedPointer::Symbol, widget_ident=4644,parent_ident="Some 4641"]
\<open>@{Symbol \<open>TemperatureSelectedPointer\<close>}\<close>
value*[IndicatedTempDRO::Label, widget_ident=4645,parent_ident="Some 4641", label_string="\<open>24\<close>"]
\<open>@{Label \<open>IndicatedTempDRO\<close>}\<close>
value*[IndicatedUnitLabel::Label, widget_ident=4645,parent_ident="Some 4641", label_string="\<open>C\<close>"]
\<open>@{Label \<open>IndicatedUnitLabel\<close>}\<close>
value*[IncreaseSelectTemp::PicturePushButton, widget_ident=4646,parent_ident="Some 4641"]
\<open>@{PicturePushButton \<open>IncreaseSelectTemp\<close>}\<close>
value*[DecreaseSelectTemp::PicturePushButton, widget_ident=4647,parent_ident="Some 4641"]
\<open>@{PicturePushButton \<open>DecreaseSelectTemp\<close>}\<close>
value*[CabinTempPanel::Panel, widget_ident=4641]
\<open>@{Panel \<open>CabinTempPanel\<close>}\<close>
value*[Layer66::Layer, layer_id=66, widgets_tree="{CabinTempPanel, DecreaseSelectTemp, IncreaseSelectTemp, IndicatedUnitLabel, IndicatedTempDRO, TemperatureSelectedPointer, TemperatureIndicatedPointer, TemperatureCelciusScale}"]
\<open>@{Layer \<open>Layer66\<close>}\<close>
value*[CabineTemperature::Window, application_id="0x6788", contained_layers="{@{Layer \<open>Layer66\<close>}}"]
\<open>@{Window \<open>CabineTemperature\<close>}\<close>
end