cc.c (12,157 bytes)
2011-10-27 17:10
#define false 0
#define true 1
typedef int bool;
#define pre(...) \at(__VA_ARGS__,P)
#define here(...) \at(__VA_ARGS__,H)
#define unchanged(x,y) (pre(x) == here(x) && pre(y) == here(y))
#define returns(x) assigns x; ensures \result == (x)
/********** tempomat_lever **********/
typedef enum {no_key, off, acc1, acc10, dec1, dec10, resume} tempomat_lever_t;
tempomat_lever_t tempomat_lever_port;
tempomat_lever_t tempomat_lever_previous_value = no_key;
/*@ predicate tempomat_lever_get_spec{P,H}(tempomat_lever_t result) = here(
(pre(tempomat_lever_port != tempomat_lever_previous_value) ==> result == tempomat_lever_port) &&
(pre(tempomat_lever_port == tempomat_lever_previous_value) ==> result == no_key));
*/
/*@ ensures tempomat_lever_get_spec{Pre,Here}(\result);
*/
tempomat_lever_t tempomat_lever_get()
{
tempomat_lever_t result;
tempomat_lever_t val = tempomat_lever_port;
if(val != tempomat_lever_previous_value) {
tempomat_lever_previous_value = val;
return val;
}
else return no_key;
}
/********** sensor **********/
typedef int speed_t;
typedef int accelerator_position_t;
//@ ghost speed_t sensor_speed_result;
/*@ returns(sensor_speed_result);
ensures 0 <= \result <= 250;
*/
speed_t sensor_speed();
//@ ghost bool sensor_brake_pedal_pressed_result;
//@ returns(sensor_brake_pedal_pressed_result);
bool sensor_brake_pedal_pressed();
//@ ghost bool sensor_engine_rpm_low_result;
//@ returns(sensor_engine_rpm_low_result);
bool sensor_engine_rpm_low();
bool sensor_driver_input_accelerate();
accelerator_position_t sensor_accelerator_position();
/********** tempomat **********/
typedef struct {
bool active;
bool temp_override;
bool previously_active;
speed_t target_speed;
#define tempomat_min_speed 30
#define tempomat_max_speed 250
} tempomat_t;
//@ ghost speed_t tempomat_previous_speed;
/*@ predicate tempomat_speed_range(integer speed) =
tempomat_min_speed <= speed <= tempomat_max_speed;
predicate tempomat_inv_speed(tempomat_t* this) =
this->active || this->previously_active ==> tempomat_speed_range(this->target_speed);
predicate tempomat_inv_prev_speed(tempomat_t* this) =
!this->active && this->previously_active ==> tempomat_previous_speed == this->target_speed;
predicate tempomat_inv0(tempomat_t* this) =
tempomat_inv_speed(this) && tempomat_inv_prev_speed(this);
predicate tempomat_active_no_temp_override(tempomat_t* this) =
this->active && !this->temp_override;
*/
#define tempomat_inv_init requires \valid(this);\
ensures tempomat_inv0(this);
#define tempomat_inv requires tempomat_inv0(this);\
tempomat_inv_init
/*@ tempomat_inv_init
*/
void tempomat_init(tempomat_t* this)
{
this->active = false;
this->previously_active = false;
}
/*@ predicate tempomat_set_spec{P,H}(tempomat_t* this, integer speed) =
( tempomat_speed_range(speed) ==> here(this->active && this->target_speed == speed)) &&
(!tempomat_speed_range(speed) ==> (unchanged(this->active, this->target_speed)));
*/
/*@ tempomat_inv
ensures tempomat_set_spec{Pre,Here}(this, speed);
*/
void tempomat_set(tempomat_t* this, speed_t speed)
{
if(tempomat_min_speed <= speed && speed <= tempomat_max_speed) {
this->active = true;
this->temp_override = false;
this->target_speed = speed;
}
}
/*@ predicate tempomat_deactivate_spec(tempomat_t* this) =
!this->active;
*/
/*@ requires this->active;
tempomat_inv
ensures tempomat_deactivate_spec(this);
*/
void tempomat_deactivate(tempomat_t* this)
{
this->active = false;
this->temp_override = false;
this->previously_active = true;
//@ ghost tempomat_previous_speed = this->target_speed;
}
//@ ghost speed_t tempomat_resume_speed;
/*@ predicate tempomat_resume_spec{P,H}(tempomat_t* this) = here(
(pre( this->previously_active) ==> this->active && this->target_speed == tempomat_previous_speed) &&
(pre(!this->previously_active) ==> tempomat_set_spec{P,H}(this, tempomat_resume_speed)));
*/
/*@ requires !this->active;
tempomat_inv
ensures tempomat_resume_spec{Pre,Here}(this);
*/
void tempomat_resume(tempomat_t* this)
{
if(this->previously_active) this->active = true;
else {
tempomat_set(this, sensor_speed());
//@ ghost tempomat_resume_speed = sensor_speed_result;
}
}
/*@ predicate tempomat_change_speed_spec{P,H}(tempomat_t* this, integer delta) =
tempomat_set_spec{P,H}(this, pre(this->target_speed) + delta);
*/
/*@ requires -20 <= delta <= 20;
requires this->active;
tempomat_inv
ensures tempomat_change_speed_spec{Pre,Here}(this, delta);
*/
void tempomat_change_speed(tempomat_t* this, speed_t delta)
{
tempomat_set(this, this->target_speed + delta);
}
//@ ghost tempomat_lever_t tempomat_handler_button;
//@ ghost speed_t tempomat_handler_speed;
//@ ghost bool tempomat_handler_brake_pedal_pressed;
//@ ghost bool tempomat_handler_engine_rpm_low;
//@ ghost bool tempomat_handler_driver_input_accelerate;
/*@ predicate deactivation_event =
tempomat_handler_button == off ||
tempomat_handler_brake_pedal_pressed ||
tempomat_handler_engine_rpm_low ||
(tempomat_handler_speed < tempomat_min_speed);
*/
/*@ predicate tempomat_handler_spec{P,H}(tempomat_t* this) = here(
tempomat_lever_get_spec{P,H}(tempomat_handler_button) &&
(deactivation_event && pre(!deactivation_event) ==> tempomat_deactivate_spec(this)) &&
(pre(this->active) ==> (
(!deactivation_event ==> (
(tempomat_handler_button == acc1 ==> tempomat_change_speed_spec{P,H}(this, 1)) &&
(tempomat_handler_button == acc10 ==> tempomat_change_speed_spec{P,H}(this, 10)) &&
(tempomat_handler_button == dec1 ==> tempomat_change_speed_spec{P,H}(this, -1)) &&
(tempomat_handler_button == dec10 ==> tempomat_change_speed_spec{P,H}(this, -10)) &&
this->active
)) &&
(tempomat_handler_driver_input_accelerate ==> !tempomat_active_no_temp_override(this))
)) &&
(pre(!this->active) ==> (
(tempomat_handler_button == acc1 || tempomat_handler_button == acc10 ||
tempomat_handler_button == dec1 || tempomat_handler_button == dec10 ==>
tempomat_set_spec{P,H}(this, tempomat_handler_speed)
) &&
(tempomat_handler_button == resume ==> tempomat_resume_spec{P,H}(this)) &&
(tempomat_handler_button != acc1 && tempomat_handler_button != acc10 &&
tempomat_handler_button != dec1 && tempomat_handler_button != dec10 &&
tempomat_handler_button != resume ==> !this->active)
)));
*/
/*@ tempomat_inv
ensures tempomat_handler_spec{Pre,Here}(this);
*/
void tempomat_handler(tempomat_t* this)
{
tempomat_lever_t button = tempomat_lever_get();
//@ ghost tempomat_handler_button = button;
if(this->active) {
switch(button) {
case acc1: tempomat_change_speed(this, 1); break;
case acc10: tempomat_change_speed(this, 10); break;
case dec1: tempomat_change_speed(this, -1); break;
case dec10: tempomat_change_speed(this, -10); break;
default: /* no action*/ break;
}
this->temp_override = sensor_driver_input_accelerate();
//@ ghost tempomat_handler_driver_input_accelerate = this->temp_override;
//@ assert tempomat_handler_driver_input_accelerate ==> !tempomat_active_no_temp_override(this);
if(button == off || sensor_brake_pedal_pressed() || sensor_engine_rpm_low() || sensor_speed() < tempomat_min_speed) {
//@ ghost tempomat_handler_brake_pedal_pressed = sensor_brake_pedal_pressed_result;
//@ ghost tempomat_handler_engine_rpm_low = sensor_engine_rpm_low_result;
//@ ghost tempomat_handler_speed = sensor_speed_result;
tempomat_deactivate(this);
//@ assert !tempomat_active_no_temp_override(this);
}
}
else {
switch(button) {
case acc1:
case acc10:
case dec1:
case dec10:
tempomat_set(this, sensor_speed());
//@ ghost tempomat_handler_speed = sensor_speed_result;
break;
case resume: tempomat_resume(this); break;
default: /* no action*/ break;
}
}
}
/********** electronic power control **********/
//@ ghost typedef enum {tempomat, accelerator} epc_input_mode_t;
//@ ghost epc_input_mode_t epc_input_mode;
/*@ assigns epc_input_mode;
ensures epc_input_mode == tempomat;
*/
void epc_input_tempomat(speed_t error);
/*@ assigns epc_input_mode;
ensures epc_input_mode == accelerator;
*/
void epc_input_manual(accelerator_position_t ap);
/********** speed_controller **********/
typedef struct {
tempomat_t tempomat;
} speed_controller_t;
/*@ predicate speed_controller_inv0(speed_controller_t* this) =
tempomat_inv0(&this->tempomat);
*/
#define speed_controller_inv_init requires \valid(this) && \valid(&this->tempomat);\
ensures speed_controller_inv0(this);
#define speed_controller_inv requires speed_controller_inv0(this);\
speed_controller_inv_init
/*@ speed_controller_inv_init
*/
void speed_controller_init(speed_controller_t* this)
{
tempomat_init(&this->tempomat);
}
/*@ predicate speed_controller_run_spec{P,H}(speed_controller_t* this) = here(
tempomat_handler_spec{P,H}(&this->tempomat) &&
( tempomat_active_no_temp_override(&this->tempomat) ==> epc_input_mode == tempomat) &&
(!tempomat_active_no_temp_override(&this->tempomat) ==> epc_input_mode == accelerator));
*/
/*@ speed_controller_inv
ensures speed_controller_run_spec{Pre,Here}(this);
*/
void speed_controller_run(speed_controller_t* this)
{
tempomat_handler(&this->tempomat);
if((&this->tempomat)->active && !(&this->tempomat)->temp_override) {
//@ assert tempomat_speed_range((&this->tempomat)->target_speed);
epc_input_tempomat((&this->tempomat)->target_speed - sensor_speed());
}
else {
epc_input_manual(sensor_accelerator_position());
}
}
/********** verification **********/
/*@ speed_controller_inv
behavior acc_dec: assumes (&this->tempomat)->active;
ensures !deactivation_event ==>
(button == acc1 ==> tempomat_change_speed_spec{Pre,Here}(&this->tempomat, 1)) &&
(button == acc10 ==> tempomat_change_speed_spec{Pre,Here}(&this->tempomat, 10)) &&
(button == dec1 ==> tempomat_change_speed_spec{Pre,Here}(&this->tempomat, -1)) &&
(button == dec10 ==> tempomat_change_speed_spec{Pre,Here}(&this->tempomat, -10));
behavior set: assumes !(&this->tempomat)->active;
ensures button == acc1 || button == acc10 || button == dec1 || button == dec10 ==>
tempomat_set_spec{Pre,Here}(&this->tempomat, tempomat_handler_speed);
behavior set_resume: assumes !(&this->tempomat)->active && !(&this->tempomat)->previously_active;
ensures button == resume ==> tempomat_set_spec{Pre,Here}(&this->tempomat, tempomat_resume_speed);
behavior resume: assumes !(&this->tempomat)->active && (&this->tempomat)->previously_active;
ensures button == resume ==> (&this->tempomat)->active && (&this->tempomat)->target_speed == tempomat_previous_speed;
behavior off: assumes button == off;
ensures deactivation_event;
behavior remains_off: assumes !(&this->tempomat)->active;
ensures button != acc1 && button != acc10 && button != dec1 && button != dec10 && button != resume ==>
!(&this->tempomat)->active;
behavior remains_on: assumes (&this->tempomat)->active;
ensures !deactivation_event ==> (&this->tempomat)->active;
*/
void speed_controller_verify_tempomat_lever_actions(speed_controller_t* this, tempomat_lever_t button)
{
tempomat_lever_previous_value = no_key;
tempomat_lever_port = button;
speed_controller_run(this);
}
/*@ speed_controller_inv
behavior deactivate: assumes !deactivation_event;
ensures deactivation_event ==> !(&this->tempomat)->active;
*/
void speed_controller_verify_deactivation(speed_controller_t* this)
{
speed_controller_run(this);
}
/*@ speed_controller_inv
ensures tempomat_active_no_temp_override(&this->tempomat) ==> epc_input_mode == tempomat;
ensures !tempomat_active_no_temp_override(&this->tempomat) ==> epc_input_mode == accelerator;
*/
void speed_controller_verify_epc_input_mode(speed_controller_t* this)
{
speed_controller_run(this);
}
/*@ speed_controller_inv
behavior override: assumes (&this->tempomat)->active;
ensures tempomat_handler_driver_input_accelerate ==> epc_input_mode == accelerator;
*/
void speed_controller_verify_override(speed_controller_t* this)
{
speed_controller_run(this);
}