Checking cspFiles/Controller.csp

Checking Test(inter(inputs(Controller),outputs(Controller)) == {}) [T= ERROR
xtrue
BEGIN TRACE example=0 process=1
error
END TRACE example=0 process=1

Checking HideAll(Controller) :[divergence free [FD]]
xtrue
BEGIN TRACE example=0 process=0

END TRACE example=0 process=0

Checking Controller :[divergence free [FD]]
true

Checking LHS_InputDet(Controller) [F= RHS_InputDet(Controller)
true

Checking LHS_OutputDec_A(Controller) [F= RHS_OutputDec_A(Controller)
true

Checking LHS_OutputDec_B(Controller,input) [F= RHS_OutputDec_B(Controller,input)
true

Checking LHS_OutputDec_B(Controller,output) [F= RHS_OutputDec_B(Controller,output)
true

Checking LHS_OutputDec_B(Controller,write) [F= RHS_OutputDec_B(Controller,write)
true

Checking LHS_OutputDec_B(Controller,read) [F= RHS_OutputDec_B(Controller,read)
true