Updated documentation and refinement headers.

models/RTS.cry

@@ -3,9 +3,9 @@
 //
 // @author Alex Bakst <[email protected]>
 // @created November, 2021
-// @refines HARDENS.sysml 
+// @refines HARDENS.sysml
 // @refines RTS.lando
-// @refines 
+// @refines RTS_Requirements.json
 
 module RTS where
 
@@ -151,6 +151,7 @@ Sense_Actuate inputs icmds rts =
     expect       = (old_vote != 0) || ShouldActuate test_ch inputs rts.instrumentation.units [i0,i1]
     test_fail    = expect != (actuators_test @ test_dev).input
 
+// @review kiniry Shouldn't this/these be private?
 MaskTripFrom: {idx} (Integral idx, Literal 0 idx) =>
   (idx -> Channel -> Bit) -> [3][4][8] -> [3][4][8]
 MaskTripFrom p trips =

models/RTS/ActuationUnit.cry

@@ -1,3 +1,13 @@
+// HARDENS Reactor Trip System (RTS) Actuation Unit
+// A formal model of RTS Actuation Unit behavior written in the
+// Cryptol DSL.
+//
+// @author Alex Bakst <[email protected]>
+// @created November, 2021
+// @refines HARDENS.sysml
+// @refines RTS.lando
+// @refines RTS_Requirements.json
+
 module RTS::ActuationUnit where
 
 import RTS::Utils

models/RTS/Actuator.cry

@@ -1,3 +1,13 @@
+// HARDENS Reactor Trip System (RTS) Actuator Unit
+// A formal model of RTS Actuator behavior written in the Cryptol
+// DSL.
+//
+// @author Alex Bakst <[email protected]>
+// @created November, 2021
+// @refines HARDENS.sysml
+// @refines RTS.lando
+// @refines RTS_Requirements.json
+
 module RTS::Actuator where
 
 type Actuation = Bit
@@ -12,7 +22,7 @@ type Actuator =
   }
 
 SetInput: Actuation -> Actuator -> Actuator
-SetInput on actuator = {actuator| input = on }
+SetInput on actuator = {actuator | input = on }
 
 SetManual: Actuation -> Actuator -> Actuator
 SetManual on actuator = {actuator | manualActuatorInput = on}

models/RTS/InstrumentationUnit.cry

@@ -1,3 +1,13 @@
+// HARDENS Reactor Trip System (RTS) Instrumentation Unit
+// A formal model of RTS Instrumentation behavior written in the
+// Cryptol DSL.
+//
+// @author Alex Bakst <[email protected]>
+// @created November, 2021
+// @refines HARDENS.sysml
+// @refines RTS.lando
+// @refines RTS_Requirements.json
+
 module RTS::InstrumentationUnit where
 
 import RTS::Utils

models/RTS/Utils.cry

@@ -1,3 +1,10 @@
+// HARDENS Reactor Trip System (RTS) Utility Functions
+// In support of a formal model of RTS system behavior written in the
+// Cryptol DSL.
+//
+// @author Alex Bakst <[email protected]>
+// @created November, 2021
+
 module RTS::Utils where
 
 infixl 5 >>>>