Skip to content
Snippets Groups Projects
Commit dee52fae authored by Alberto Debiasi's avatar Alberto Debiasi
Browse files

Update oracles in regression test with CleanC.

Change-Id: I1a088d7b666bd6c8f5d3b5e0a265d4ceda337fa5
parent beca2a69
No related branches found
No related tags found
No related merge requests found
......@@ -18,6 +18,6 @@ MODULE main
esac ;
next ( absence_alarm ) :=
case
Transition = pr_to_pr & ( TRUE ) : ( !next(input_is_present) & next(enabled)) ;
Transition = pr_to_pr & ( TRUE ) : ! input_is_present & enabled = TRUE ;
TRUE : absence_alarm ;
esac ;
......@@ -16,8 +16,8 @@ MODULE main
Transition : { in1_to_in1 , in1_to_in2 , in2_to_in1 , in2_to_in2 } ;
INIT ( InitTransition = init_to_in1 -> State = input_1 )
TRANS Transition = in1_to_in1 -> ( ( ! switch_current_use ) & State = input_1 & next ( State ) = input_1 )
TRANS Transition = in1_to_in2 -> ( ( switch_current_use ) & State = input_1 & next ( State ) = input_2 )
TRANS Transition = in2_to_in1 -> ( ( switch_current_use ) & State = input_2 & next ( State ) = input_1 )
TRANS Transition = in1_to_in2 -> ( ( switch_current_use = TRUE ) & State = input_1 & next ( State ) = input_2 )
TRANS Transition = in2_to_in1 -> ( ( switch_current_use = TRUE ) & State = input_2 & next ( State ) = input_1 )
TRANS Transition = in2_to_in2 -> ( ( ! switch_current_use ) & State = input_2 & next ( State ) = input_2 )
ASSIGN
init ( current_use ) :=
......@@ -34,23 +34,23 @@ MODULE main
esac ;
next ( current_use ) :=
case
Transition = in1_to_in2 & ( switch_current_use ) : 2 ;
Transition = in2_to_in1 & ( switch_current_use ) : 1 ;
Transition = in1_to_in2 & ( switch_current_use = TRUE ) : 2 ;
Transition = in2_to_in1 & ( switch_current_use = TRUE ) : 1 ;
TRUE : current_use ;
esac ;
next ( output ) :=
case
Transition = in1_to_in1 & ( ! switch_current_use ) : input1 ;
Transition = in1_to_in2 & ( switch_current_use ) : input2 ;
Transition = in2_to_in1 & ( switch_current_use ) : input1 ;
Transition = in1_to_in2 & ( switch_current_use = TRUE ) : input2 ;
Transition = in2_to_in1 & ( switch_current_use = TRUE ) : input1 ;
Transition = in2_to_in2 & ( ! switch_current_use ) : input2 ;
TRUE : output ;
esac ;
next ( output_is_present ) :=
case
Transition = in1_to_in1 & ( ! switch_current_use ) : input1_is_present ;
Transition = in1_to_in2 & ( switch_current_use ) : input2_is_present ;
Transition = in2_to_in1 & ( switch_current_use ) : input1_is_present ;
Transition = in1_to_in2 & ( switch_current_use = TRUE ) : input2_is_present ;
Transition = in2_to_in1 & ( switch_current_use = TRUE ) : input1_is_present ;
Transition = in2_to_in2 & ( ! switch_current_use ) : input2_is_present ;
TRUE : output_is_present ;
esac ;
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment