smyalygames/checklist-tester
1
0
Fork 0
mirror of https://github.com/smyalygames/checklist-tester.git synced 2025-05-18 14:34:12 +02:00
Code Issues Actions Packages Projects Releases Wiki Activity

feat(connector): add VDM type data class for ItemObject

Browse Source
This commit is contained in:
Anthony Berg 2024-05-07 12:14:32 +01:00
parent 34904c4bf8
commit 51269484af
3 changed files with 15 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
connector/shared/src/commonMain/kotlin/io/anthonyberg/connector/shared/vdmj/type/Aircraft.kt
View File

@ -4,7 +4,7 @@ package io.anthonyberg.connector.shared.vdmj.type
* Aircraft record type in the VDM-SL model * Aircraft record type in the VDM-SL model
*/ */
data class Aircraft( data class Aircraft(
val items: Map<String, Switch>, // TODO value should be ItemObject type val items: Map<String, ItemObject>,
val procedure: MutableList<ProcedureItem> val procedure: MutableList<ProcedureItem>
) { ) {
/** /**

13
connector/shared/src/commonMain/kotlin/io/anthonyberg/connector/shared/vdmj/type/ItemObject.kt Normal file
View File

@ -0,0 +1,13 @@
package io.anthonyberg.connector.shared.vdmj.type
data class ItemObject(val type: ItemType, val item: Switch) { // TODO add types for other items
/**
* Converts to String for a VDM representation of an ItemObject record
*
* @return String representation for VDM ItemObject
*/
fun toVDMString(): String {
return "mk_ItemObject(${type.toVDMString()}, ${item.toVDMString()})"
}
}

11
connector/shared/src/commonMain/kotlin/io/anthonyberg/connector/shared/vdmj/type/Switch.kt
View File

@ -12,21 +12,12 @@ data class Switch(val position: Int, val middlePosition: Boolean = false) {
require((position >= 0) and ((position <= 1) and !middlePosition) or ((position <= 2) and middlePosition)) require((position >= 0) and ((position <= 1) and !middlePosition) or ((position <= 2) and middlePosition))
} }
/**
* Converts to String for a VDM representation of an ItemObject record
*
* @return String representation for VDM ItemObject
*/
fun toVDMString(): String {
return "mk_ItemObject(<SWITCH>, ${toSwitchVDMString()})"
}
/** /**
* Converts to String for a VDM representation of a Switch record * Converts to String for a VDM representation of a Switch record
* *
* @return String representation for VDM Switch * @return String representation for VDM Switch
*/ */
private fun toSwitchVDMString(): String { fun toVDMString(): String {
return "mk_Switch(${getSwitchState()}, $middlePosition)" return "mk_Switch(${getSwitchState()}, $middlePosition)"
} }