Checking cspFiles/Cell.csp Checking Test(inter(inputs(Cell),outputs(Cell)) == {}) [T= ERROR xtrue BEGIN TRACE example=0 process=1 error END TRACE example=0 process=1 Checking HideAll(Cell) :[divergence free [FD]] xtrue BEGIN TRACE example=0 process=0 END TRACE example=0 process=0 Checking Cell :[divergence free [FD]] true Checking LHS_InputDet(Cell) [F= RHS_InputDet(Cell) true Checking LHS_OutputDec_A(Cell) [F= RHS_OutputDec_A(Cell) true Checking LHS_OutputDec_B(Cell,rd) [F= RHS_OutputDec_B(Cell,rd) true Checking LHS_OutputDec_B(Cell,wrt) [F= RHS_OutputDec_B(Cell,wrt) true