mirror of
				https://github.com/smyalygames/checklist-tester.git
				synced 2025-11-04 04:49:49 +01:00 
			
		
		
		
	feat(connector): add VDM type data class for Switch
This commit is contained in:
		
							parent
							
								
									08da2d4506
								
							
						
					
					
						commit
						21c597b3dc
					
				@ -4,7 +4,7 @@ package io.anthonyberg.connector.shared.vdmj.type
 | 
			
		||||
 * Aircraft record type in the VDM-SL model
 | 
			
		||||
 */
 | 
			
		||||
data class Aircraft(
 | 
			
		||||
    val items: Map<String, String>, // TODO value should be ItemObject type
 | 
			
		||||
    val items: Map<String, Switch>, // TODO value should be ItemObject type
 | 
			
		||||
    val procedure: MutableList<String> // TODO change String to a ProcedureItem type
 | 
			
		||||
) {
 | 
			
		||||
    /**
 | 
			
		||||
@ -33,8 +33,7 @@ data class Aircraft(
 | 
			
		||||
        for (dref: String in items.keys) {
 | 
			
		||||
            val value = items.getValue(dref)
 | 
			
		||||
 | 
			
		||||
            // TODO make sure to run toString on value once items Map changes the value type
 | 
			
		||||
            output += "\"$dref\" |-> $value,"
 | 
			
		||||
            output += "\"$dref\" |-> ${value.toVDMString()},"
 | 
			
		||||
        }
 | 
			
		||||
 | 
			
		||||
        // Removes the last comma in the VDM map as it will error otherwise
 | 
			
		||||
 | 
			
		||||
@ -0,0 +1,46 @@
 | 
			
		||||
package io.anthonyberg.connector.shared.vdmj.type
 | 
			
		||||
 | 
			
		||||
/**
 | 
			
		||||
 * Switch record type in VDM-SL
 | 
			
		||||
 *
 | 
			
		||||
 * @param position Position of the switch
 | 
			
		||||
 * @param middlePosition `true` if there is a middle position for the switch,
 | 
			
		||||
 * `false` if the switch only has 2 positions
 | 
			
		||||
 */
 | 
			
		||||
data class Switch(val position: Int, val middlePosition: Boolean = false) {
 | 
			
		||||
    init {
 | 
			
		||||
        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
 | 
			
		||||
     *
 | 
			
		||||
     * @return String representation for VDM Switch
 | 
			
		||||
     */
 | 
			
		||||
    private fun toSwitchVDMString(): String {
 | 
			
		||||
        return "mk_Switch(${getSwitchState()}, $middlePosition)"
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    /**
 | 
			
		||||
     * Gets the VDM object for the switch state
 | 
			
		||||
     *
 | 
			
		||||
     * @return String representation for switch state
 | 
			
		||||
     */
 | 
			
		||||
    private fun getSwitchState(): String {
 | 
			
		||||
        return when (position) {
 | 
			
		||||
            0 -> "<OFF>"
 | 
			
		||||
            1 -> if (middlePosition) "<MIDDLE>" else "<ON>"
 | 
			
		||||
            2 -> "<ON>"
 | 
			
		||||
            else -> throw IllegalArgumentException("Position must be between 0 and 2")
 | 
			
		||||
        }
 | 
			
		||||
    }
 | 
			
		||||
}
 | 
			
		||||
		Loading…
	
	
			
			x
			
			
		
	
		Reference in New Issue
	
	Block a user