extern void abort(void); extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); void reach_error() { __assert_fail("0", "rekh_nxt.1.M1-1.c", 3, "reach_error"); } // This file is part of the SV-Benchmarks collection of verification tasks: // https://github.com/sosy-lab/sv-benchmarks // // SPDX-FileCopyrightText: 2013 Carnegie Mellon University // SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community // // SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU /* Generated by CIL v. 1.4.0 */ /* print_CIL_Input is true */ unsigned char __startrek_start[27] ; unsigned char __startrek_end[27] ; unsigned char __startrek_max[27] ; unsigned char __startrek_min[27] ; void __startrek_init_shared(void) ; __inline static _Bool __startrek_cs_t2(void) ; __inline static _Bool __startrek_cs_t1(void) ; __inline static _Bool __startrek_cs_t0(void) ; _Bool __VERIFIER_nondet_bool(void) ; unsigned char __VERIFIER_nondet_uchar(void) ; _Bool __VERIFIER_nondet_bool(void) ; extern int __VERIFIER_nondet_int(); void abort(void); void assume_abort_if_not(int cond) { if(!cond) {abort();} } unsigned char __startrek_round ; unsigned char __startrek_task ; unsigned char __startrek_job ; unsigned char __startrek_job_end ; _Bool __startrek_lock = (_Bool)0; unsigned char __startrek_hyper_period ; #pragma merger(0,"/tmp/aaaa/nxt.bug1.i","-S") void assert(_Bool arg) { if (!arg) { ERROR: {reach_error();abort();}} } static unsigned int ud_err_theta ; static unsigned int ud_psi ; static unsigned int ud_theta_lpf ; static unsigned int ud_theta_ref ; static unsigned int ud_thetadot_cmd_lpf ; extern unsigned int A_D ; extern unsigned int A_R ; extern unsigned int K_F[4] ; extern unsigned int K_I ; extern unsigned int K_PHIDOT ; extern unsigned int K_THETADOT ; extern unsigned int const BATTERY_GAIN ; extern unsigned int const BATTERY_OFFSET ; void balance_init(void) { { ud_err_theta = 0.0F; ud_theta_ref = 0.0F; ud_thetadot_cmd_lpf = 0.0F; ud_psi = 0.0F; ud_theta_lpf = 0.0F; return; } } void balance_control(unsigned int args_cmd_forward , unsigned int args_cmd_turn , unsigned int args_gyro , unsigned int args_gyro_offset , unsigned int args_theta_m_l , unsigned int args_theta_m_r , unsigned int args_battery , char *ret_pwm_l , char *ret_pwm_r ) { unsigned int tmp_theta ; unsigned int tmp_theta_lpf ; unsigned int tmp_pwm_r_limiter ; unsigned int tmp_psidot ; unsigned int tmp_pwm_turn ; unsigned int tmp_pwm_l_limiter ; unsigned int tmp_thetadot_cmd_lpf ; unsigned int tmp[4] ; unsigned int tmp_theta_0[4] ; int tmp_0 ; int tmp___0 ; int tmp___1 ; { tmp_thetadot_cmd_lpf = (((float )args_cmd_forward / 100.0F) * (float )K_THETADOT) * (1.0F - (float )A_R) + (float )(A_R * ud_thetadot_cmd_lpf); tmp_theta = ((0.01745329238F * (float )args_theta_m_l + (float )ud_psi) + (0.01745329238F * (float )args_theta_m_r + (float )ud_psi)) * 0.5F; tmp_theta_lpf = (1.0F - (float )A_D) * (float )tmp_theta + (float )(A_D * ud_theta_lpf); tmp_psidot = (float )(args_gyro - args_gyro_offset) * 0.01745329238F; tmp[0] = ud_theta_ref; tmp[1] = 0.0F; tmp[2] = tmp_thetadot_cmd_lpf; tmp[3] = 0.0F; tmp_theta_0[0] = tmp_theta; tmp_theta_0[1] = ud_psi; tmp_theta_0[2] = (float )(tmp_theta_lpf - ud_theta_lpf) / 0.00400000019F; tmp_theta_0[3] = tmp_psidot; tmp_pwm_r_limiter = 0.0F; tmp_0 = 0; tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0]; tmp_0 ++; tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0]; tmp_0 ++; tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0]; tmp_0 ++; tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0]; tmp_0 ++; assume_abort_if_not(((BATTERY_GAIN*args_battery) - BATTERY_OFFSET) != 0); tmp_pwm_r_limiter = (float )((K_I * ud_err_theta + tmp_pwm_r_limiter) / (unsigned int )(BATTERY_GAIN * (unsigned int const )args_battery - BATTERY_OFFSET)) * 100.0F; tmp_pwm_turn = ((float )args_cmd_turn / 100.0F) * (float )K_PHIDOT; tmp_pwm_l_limiter = tmp_pwm_r_limiter + tmp_pwm_turn; tmp___0 = __VERIFIER_nondet_int(); tmp_pwm_l_limiter = tmp___0; *ret_pwm_l = (char )tmp_pwm_l_limiter; tmp_pwm_r_limiter -= tmp_pwm_turn; tmp___1 = __VERIFIER_nondet_int(); tmp_pwm_r_limiter = tmp___1; *ret_pwm_r = (char )tmp_pwm_r_limiter; tmp_pwm_l_limiter = 0.00400000019F * (float )tmp_thetadot_cmd_lpf + (float )ud_theta_ref; tmp_pwm_turn = 0.00400000019F * (float )tmp_psidot + (float )ud_psi; tmp_pwm_r_limiter = (float )(ud_theta_ref - tmp_theta) * 0.00400000019F + (float )ud_err_theta; ud_err_theta = tmp_pwm_r_limiter; ud_theta_ref = tmp_pwm_l_limiter; ud_thetadot_cmd_lpf = tmp_thetadot_cmd_lpf; ud_psi = tmp_pwm_turn; ud_theta_lpf = tmp_theta_lpf; return; } } extern unsigned int __VERIFIER_nondet_uint() ; extern char __VERIFIER_nondet_char() ; extern unsigned char __VERIFIER_nondet_uchar() ; __inline static unsigned char __startrek_read_nxtway_gs_mode(void) ; __inline static void __startrek_write_nxtway_gs_mode(unsigned char arg ) ; unsigned char _nxtway_gs_mode_[27] ; unsigned char _i_nxtway_gs_mode_[27] ; unsigned char __startrek_hidden_nxtway_gs_mode = 0; __inline static _Bool __startrek_read_obstacle_flag(void) ; __inline static void __startrek_write_obstacle_flag(_Bool arg ) ; _Bool _obstacle_flag_[27] ; _Bool _i_obstacle_flag_[27] ; _Bool __startrek_hidden_obstacle_flag = 0; extern void nxt_motor_set_count(unsigned char port , char pwm ) ; char nxt_motor_get_count(unsigned char port ) { char tmp ; { tmp = __VERIFIER_nondet_char(); return (tmp); } } unsigned int ecrobot_get_systick_ms(void) ; static unsigned int timer = 0; unsigned int ecrobot_get_systick_ms(void) { unsigned int r ; { r = timer; timer += 1000U; return (r); } } unsigned int ecrobot_get_gyro_sensor(unsigned char port ) { unsigned int tmp ; { tmp = __VERIFIER_nondet_uint(); return (tmp); } } extern void ecrobot_sound_tone(unsigned int , unsigned int , char ) ; extern void ecrobot_status_monitor(char * ) ; void ecrobot_read_bt_packet(unsigned char *bt_receive_buf , unsigned char sz ) { { *(bt_receive_buf + 0) = __VERIFIER_nondet_uchar(); *(bt_receive_buf + 1) = __VERIFIER_nondet_uchar(); return; } } unsigned int ecrobot_get_battery_voltage(void) { unsigned int tmp ; { tmp = __VERIFIER_nondet_uint(); return (tmp); } } extern void nxt_motor_set_speed(unsigned char port , char speed , char one ) ; extern void ecrobot_bt_data_logger(char , char ) ; static unsigned int gyro_offset ; static unsigned int avg_cnt ; static unsigned int cal_start_time ; static unsigned char bt_receive_buf[2] ; void OSEK_Task_ts1(void) { int i ; char cmd_forward ; char cmd_turn ; char pwm_l ; char pwm_r ; unsigned char tmp ; unsigned int tmp___0 ; unsigned int tmp___1 ; _Bool tmp___2 ; unsigned int tmp___3 ; char tmp___4 ; char tmp___5 ; unsigned int tmp___6 ; { tmp = __startrek_read_nxtway_gs_mode(); switch (tmp) { case 0: gyro_offset = 0; avg_cnt = 0; i = 0; while (i < 2) { bt_receive_buf[i] = 0; i ++; } balance_init(); nxt_motor_set_count(0, 0); nxt_motor_set_count(1, 0); cal_start_time = ecrobot_get_systick_ms(); __startrek_write_nxtway_gs_mode(1); break; case 1: tmp___0 = ecrobot_get_gyro_sensor(3); gyro_offset += tmp___0; avg_cnt ++; tmp___1 = ecrobot_get_systick_ms(); if (tmp___1 - cal_start_time >= 1000U) { assume_abort_if_not(avg_cnt != 0); gyro_offset /= avg_cnt; ecrobot_sound_tone(440U, 500U, 30); __startrek_write_nxtway_gs_mode(2); } break; case 2: ecrobot_read_bt_packet(bt_receive_buf, 2); cmd_forward = - ((int )((char )bt_receive_buf[0])); cmd_turn = (char )bt_receive_buf[1]; tmp___2 = __startrek_read_obstacle_flag(); if (tmp___2) { cmd_forward = -100; cmd_turn = 0; } tmp___3 = ecrobot_get_battery_voltage(); tmp___4 = nxt_motor_get_count(1); tmp___5 = nxt_motor_get_count(0); tmp___6 = ecrobot_get_gyro_sensor(3); balance_control((unsigned int )cmd_forward, (unsigned int )cmd_turn, tmp___6, gyro_offset, (unsigned int )tmp___5, (unsigned int )tmp___4, tmp___3, & pwm_l, & pwm_r); nxt_motor_set_speed(0, pwm_l, 1); nxt_motor_set_speed(1, pwm_r, 1); ecrobot_bt_data_logger(cmd_forward, cmd_turn); break; default: nxt_motor_set_speed(0, 0, 1); nxt_motor_set_speed(1, 0, 1); break; } return; } } unsigned char ecrobot_get_sonar_sensor(unsigned char port ) { unsigned char tmp ; { tmp = __VERIFIER_nondet_uchar(); return (tmp); } } void OSEK_Task_ts2(void) { unsigned char tmp ; unsigned char tmp___0 ; { __startrek_write_obstacle_flag(0); tmp = __startrek_read_nxtway_gs_mode(); if (tmp == 2) { tmp___0 = ecrobot_get_sonar_sensor(4); if ((int )tmp___0 <= 25) { __startrek_write_obstacle_flag(1); } } return; } } __inline void __startrek_user_final(void) { int tmp ; { tmp = _nxtway_gs_mode_[26]; assert(tmp != 2); return; } } char __startrek_base_priority_OSEK_Task_ts2 = 1; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts2(void) ; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts2(void) { { OSEK_Task_ts2(); return ((_Bool)1); } } void cil_keeperOSEK_Task_ts2(void) { { __startrek_entry_pt_OSEK_Task_ts2(); return; } } int __startrek_period_OSEK_Task_ts2 = 48; int __startrek_wcet_OSEK_Task_ts2 = 4; int __startrek_arrival_min_OSEK_Task_ts2 = 0; int __startrek_arrival_max_OSEK_Task_ts2 = 0; char __startrek_base_priority_OSEK_Task_ts1 = 2; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts1(void) ; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts1(void) { { OSEK_Task_ts1(); return ((_Bool)1); } } void cil_keeperOSEK_Task_ts1(void) { { __startrek_entry_pt_OSEK_Task_ts1(); return; } } int __startrek_period_OSEK_Task_ts1 = 4; int __startrek_wcet_OSEK_Task_ts1 = 1; int __startrek_arrival_min_OSEK_Task_ts1 = 0; int __startrek_arrival_max_OSEK_Task_ts1 = 0; extern void write_mode_on_lcd(unsigned char m ) ; void OSEK_Task_Background(void) { unsigned char m ; unsigned char tmp ; { tmp = __startrek_read_nxtway_gs_mode(); m = tmp; ecrobot_status_monitor("NXTway-GS"); write_mode_on_lcd(m); return; } } char __startrek_base_priority_OSEK_Task_Background = 0; __inline static _Bool __startrek_entry_pt_OSEK_Task_Background(void) ; __inline static _Bool __startrek_entry_pt_OSEK_Task_Background(void) { { OSEK_Task_Background(); return ((_Bool)1); } } void cil_keeperOSEK_Task_Background(void) { { __startrek_entry_pt_OSEK_Task_Background(); return; } } int __startrek_period_OSEK_Task_Background = 96; int __startrek_wcet_OSEK_Task_Background = 3; int __startrek_arrival_min_OSEK_Task_Background = 0; int __startrek_arrival_max_OSEK_Task_Background = 0; int __startrek_time_bound = 96; __inline void __startrek_schedule_jobs(void) { { __startrek_start[26] = __VERIFIER_nondet_uchar(); __startrek_end[26] = __VERIFIER_nondet_uchar(); __startrek_min[26] = __VERIFIER_nondet_uchar(); __startrek_max[26] = __VERIFIER_nondet_uchar(); __startrek_start[25] = __VERIFIER_nondet_uchar(); __startrek_end[25] = __VERIFIER_nondet_uchar(); __startrek_min[25] = __VERIFIER_nondet_uchar(); __startrek_max[25] = __VERIFIER_nondet_uchar(); __startrek_start[24] = __VERIFIER_nondet_uchar(); __startrek_end[24] = __VERIFIER_nondet_uchar(); __startrek_min[24] = __VERIFIER_nondet_uchar(); __startrek_max[24] = __VERIFIER_nondet_uchar(); __startrek_start[23] = __VERIFIER_nondet_uchar(); __startrek_end[23] = __VERIFIER_nondet_uchar(); __startrek_min[23] = __VERIFIER_nondet_uchar(); __startrek_max[23] = __VERIFIER_nondet_uchar(); __startrek_start[22] = __VERIFIER_nondet_uchar(); __startrek_end[22] = __VERIFIER_nondet_uchar(); __startrek_min[22] = __VERIFIER_nondet_uchar(); __startrek_max[22] = __VERIFIER_nondet_uchar(); __startrek_start[21] = __VERIFIER_nondet_uchar(); __startrek_end[21] = __VERIFIER_nondet_uchar(); __startrek_min[21] = __VERIFIER_nondet_uchar(); __startrek_max[21] = __VERIFIER_nondet_uchar(); __startrek_start[20] = __VERIFIER_nondet_uchar(); __startrek_end[20] = __VERIFIER_nondet_uchar(); __startrek_min[20] = __VERIFIER_nondet_uchar(); __startrek_max[20] = __VERIFIER_nondet_uchar(); __startrek_start[19] = __VERIFIER_nondet_uchar(); __startrek_end[19] = __VERIFIER_nondet_uchar(); __startrek_min[19] = __VERIFIER_nondet_uchar(); __startrek_max[19] = __VERIFIER_nondet_uchar(); __startrek_start[18] = __VERIFIER_nondet_uchar(); __startrek_end[18] = __VERIFIER_nondet_uchar(); __startrek_min[18] = __VERIFIER_nondet_uchar(); __startrek_max[18] = __VERIFIER_nondet_uchar(); __startrek_start[17] = __VERIFIER_nondet_uchar(); __startrek_end[17] = __VERIFIER_nondet_uchar(); __startrek_min[17] = __VERIFIER_nondet_uchar(); __startrek_max[17] = __VERIFIER_nondet_uchar(); __startrek_start[16] = __VERIFIER_nondet_uchar(); __startrek_end[16] = __VERIFIER_nondet_uchar(); __startrek_min[16] = __VERIFIER_nondet_uchar(); __startrek_max[16] = __VERIFIER_nondet_uchar(); __startrek_start[15] = __VERIFIER_nondet_uchar(); __startrek_end[15] = __VERIFIER_nondet_uchar(); __startrek_min[15] = __VERIFIER_nondet_uchar(); __startrek_max[15] = __VERIFIER_nondet_uchar(); __startrek_start[14] = __VERIFIER_nondet_uchar(); __startrek_end[14] = __VERIFIER_nondet_uchar(); __startrek_min[14] = __VERIFIER_nondet_uchar(); __startrek_max[14] = __VERIFIER_nondet_uchar(); __startrek_start[13] = __VERIFIER_nondet_uchar(); __startrek_end[13] = __VERIFIER_nondet_uchar(); __startrek_min[13] = __VERIFIER_nondet_uchar(); __startrek_max[13] = __VERIFIER_nondet_uchar(); __startrek_start[12] = __VERIFIER_nondet_uchar(); __startrek_end[12] = __VERIFIER_nondet_uchar(); __startrek_min[12] = __VERIFIER_nondet_uchar(); __startrek_max[12] = __VERIFIER_nondet_uchar(); __startrek_start[11] = __VERIFIER_nondet_uchar(); __startrek_end[11] = __VERIFIER_nondet_uchar(); __startrek_min[11] = __VERIFIER_nondet_uchar(); __startrek_max[11] = __VERIFIER_nondet_uchar(); __startrek_start[10] = __VERIFIER_nondet_uchar(); __startrek_end[10] = __VERIFIER_nondet_uchar(); __startrek_min[10] = __VERIFIER_nondet_uchar(); __startrek_max[10] = __VERIFIER_nondet_uchar(); __startrek_start[9] = __VERIFIER_nondet_uchar(); __startrek_end[9] = __VERIFIER_nondet_uchar(); __startrek_min[9] = __VERIFIER_nondet_uchar(); __startrek_max[9] = __VERIFIER_nondet_uchar(); __startrek_start[8] = __VERIFIER_nondet_uchar(); __startrek_end[8] = __VERIFIER_nondet_uchar(); __startrek_min[8] = __VERIFIER_nondet_uchar(); __startrek_max[8] = __VERIFIER_nondet_uchar(); __startrek_start[7] = __VERIFIER_nondet_uchar(); __startrek_end[7] = __VERIFIER_nondet_uchar(); __startrek_min[7] = __VERIFIER_nondet_uchar(); __startrek_max[7] = __VERIFIER_nondet_uchar(); __startrek_start[6] = __VERIFIER_nondet_uchar(); __startrek_end[6] = __VERIFIER_nondet_uchar(); __startrek_min[6] = __VERIFIER_nondet_uchar(); __startrek_max[6] = __VERIFIER_nondet_uchar(); __startrek_start[5] = __VERIFIER_nondet_uchar(); __startrek_end[5] = __VERIFIER_nondet_uchar(); __startrek_min[5] = __VERIFIER_nondet_uchar(); __startrek_max[5] = __VERIFIER_nondet_uchar(); __startrek_start[4] = __VERIFIER_nondet_uchar(); __startrek_end[4] = __VERIFIER_nondet_uchar(); __startrek_min[4] = __VERIFIER_nondet_uchar(); __startrek_max[4] = __VERIFIER_nondet_uchar(); __startrek_start[3] = __VERIFIER_nondet_uchar(); __startrek_end[3] = __VERIFIER_nondet_uchar(); __startrek_min[3] = __VERIFIER_nondet_uchar(); __startrek_max[3] = __VERIFIER_nondet_uchar(); __startrek_start[2] = __VERIFIER_nondet_uchar(); __startrek_end[2] = __VERIFIER_nondet_uchar(); __startrek_min[2] = __VERIFIER_nondet_uchar(); __startrek_max[2] = __VERIFIER_nondet_uchar(); __startrek_start[1] = __VERIFIER_nondet_uchar(); __startrek_end[1] = __VERIFIER_nondet_uchar(); __startrek_min[1] = __VERIFIER_nondet_uchar(); __startrek_max[1] = __VERIFIER_nondet_uchar(); __startrek_start[0] = __VERIFIER_nondet_uchar(); __startrek_end[0] = __VERIFIER_nondet_uchar(); __startrek_min[0] = __VERIFIER_nondet_uchar(); __startrek_max[0] = __VERIFIER_nondet_uchar(); assume_abort_if_not(24 <= __startrek_start[26]); assume_abort_if_not(__startrek_end[26] <= 26); assume_abort_if_not(__startrek_start[26] == __startrek_end[26]); assume_abort_if_not(__startrek_min[26] == __startrek_start[26]); assume_abort_if_not(__startrek_max[26] == __startrek_end[26]); assume_abort_if_not(23 <= __startrek_start[25]); assume_abort_if_not(__startrek_end[25] <= 25); assume_abort_if_not(__startrek_max[25] < __startrek_min[26]); assume_abort_if_not(__startrek_start[25] == __startrek_end[25]); assume_abort_if_not(__startrek_min[25] == __startrek_start[25]); assume_abort_if_not(__startrek_max[25] == __startrek_end[25]); assume_abort_if_not(22 <= __startrek_start[24]); assume_abort_if_not(__startrek_end[24] <= 24); assume_abort_if_not(__startrek_max[24] < __startrek_min[25]); assume_abort_if_not(__startrek_start[24] == __startrek_end[24]); assume_abort_if_not(__startrek_min[24] == __startrek_start[24]); assume_abort_if_not(__startrek_max[24] == __startrek_end[24]); assume_abort_if_not(21 <= __startrek_start[23]); assume_abort_if_not(__startrek_end[23] <= 23); assume_abort_if_not(__startrek_max[23] < __startrek_min[24]); assume_abort_if_not(__startrek_start[23] == __startrek_end[23]); assume_abort_if_not(__startrek_min[23] == __startrek_start[23]); assume_abort_if_not(__startrek_max[23] == __startrek_end[23]); assume_abort_if_not(20 <= __startrek_start[22]); assume_abort_if_not(__startrek_end[22] <= 22); assume_abort_if_not(__startrek_max[22] < __startrek_min[23]); assume_abort_if_not(__startrek_start[22] == __startrek_end[22]); assume_abort_if_not(__startrek_min[22] == __startrek_start[22]); assume_abort_if_not(__startrek_max[22] == __startrek_end[22]); assume_abort_if_not(19 <= __startrek_start[21]); assume_abort_if_not(__startrek_end[21] <= 21); assume_abort_if_not(__startrek_max[21] < __startrek_min[22]); assume_abort_if_not(__startrek_start[21] == __startrek_end[21]); assume_abort_if_not(__startrek_min[21] == __startrek_start[21]); assume_abort_if_not(__startrek_max[21] == __startrek_end[21]); assume_abort_if_not(18 <= __startrek_start[20]); assume_abort_if_not(__startrek_end[20] <= 20); assume_abort_if_not(__startrek_max[20] < __startrek_min[21]); assume_abort_if_not(__startrek_start[20] == __startrek_end[20]); assume_abort_if_not(__startrek_min[20] == __startrek_start[20]); assume_abort_if_not(__startrek_max[20] == __startrek_end[20]); assume_abort_if_not(17 <= __startrek_start[19]); assume_abort_if_not(__startrek_end[19] <= 19); assume_abort_if_not(__startrek_max[19] < __startrek_min[20]); assume_abort_if_not(__startrek_start[19] == __startrek_end[19]); assume_abort_if_not(__startrek_min[19] == __startrek_start[19]); assume_abort_if_not(__startrek_max[19] == __startrek_end[19]); assume_abort_if_not(16 <= __startrek_start[18]); assume_abort_if_not(__startrek_end[18] <= 18); assume_abort_if_not(__startrek_max[18] < __startrek_min[19]); assume_abort_if_not(__startrek_start[18] == __startrek_end[18]); assume_abort_if_not(__startrek_min[18] == __startrek_start[18]); assume_abort_if_not(__startrek_max[18] == __startrek_end[18]); assume_abort_if_not(15 <= __startrek_start[17]); assume_abort_if_not(__startrek_end[17] <= 17); assume_abort_if_not(__startrek_max[17] < __startrek_min[18]); assume_abort_if_not(__startrek_start[17] == __startrek_end[17]); assume_abort_if_not(__startrek_min[17] == __startrek_start[17]); assume_abort_if_not(__startrek_max[17] == __startrek_end[17]); assume_abort_if_not(14 <= __startrek_start[16]); assume_abort_if_not(__startrek_end[16] <= 16); assume_abort_if_not(__startrek_max[16] < __startrek_min[17]); assume_abort_if_not(__startrek_start[16] == __startrek_end[16]); assume_abort_if_not(__startrek_min[16] == __startrek_start[16]); assume_abort_if_not(__startrek_max[16] == __startrek_end[16]); assume_abort_if_not(13 <= __startrek_start[15]); assume_abort_if_not(__startrek_end[15] <= 15); assume_abort_if_not(__startrek_max[15] < __startrek_min[16]); assume_abort_if_not(__startrek_start[15] == __startrek_end[15]); assume_abort_if_not(__startrek_min[15] == __startrek_start[15]); assume_abort_if_not(__startrek_max[15] == __startrek_end[15]); assume_abort_if_not(13 <= __startrek_start[14]); assume_abort_if_not(__startrek_end[14] <= 26); assume_abort_if_not(__startrek_start[14] <= __startrek_end[14]); if (__startrek_start[14] < __startrek_min[15]) { assume_abort_if_not(__startrek_min[14] == __startrek_start[14]); } else { assume_abort_if_not(__startrek_min[14] == __startrek_min[15]); } if (__startrek_end[14] > __startrek_max[26]) { assume_abort_if_not(__startrek_max[14] == __startrek_end[14]); } else { assume_abort_if_not(__startrek_max[14] == __startrek_max[26]); } assume_abort_if_not(11 <= __startrek_start[13]); assume_abort_if_not(__startrek_end[13] <= 13); assume_abort_if_not(__startrek_start[13] == __startrek_end[13]); assume_abort_if_not(__startrek_min[13] == __startrek_start[13]); assume_abort_if_not(__startrek_max[13] == __startrek_end[13]); assume_abort_if_not(10 <= __startrek_start[12]); assume_abort_if_not(__startrek_end[12] <= 12); assume_abort_if_not(__startrek_max[12] < __startrek_min[13]); assume_abort_if_not(__startrek_start[12] == __startrek_end[12]); assume_abort_if_not(__startrek_min[12] == __startrek_start[12]); assume_abort_if_not(__startrek_max[12] == __startrek_end[12]); assume_abort_if_not(9 <= __startrek_start[11]); assume_abort_if_not(__startrek_end[11] <= 11); assume_abort_if_not(__startrek_max[11] < __startrek_min[12]); assume_abort_if_not(__startrek_start[11] == __startrek_end[11]); assume_abort_if_not(__startrek_min[11] == __startrek_start[11]); assume_abort_if_not(__startrek_max[11] == __startrek_end[11]); assume_abort_if_not(8 <= __startrek_start[10]); assume_abort_if_not(__startrek_end[10] <= 10); assume_abort_if_not(__startrek_max[10] < __startrek_min[11]); assume_abort_if_not(__startrek_start[10] == __startrek_end[10]); assume_abort_if_not(__startrek_min[10] == __startrek_start[10]); assume_abort_if_not(__startrek_max[10] == __startrek_end[10]); assume_abort_if_not(7 <= __startrek_start[9]); assume_abort_if_not(__startrek_end[9] <= 9); assume_abort_if_not(__startrek_max[9] < __startrek_min[10]); assume_abort_if_not(__startrek_start[9] == __startrek_end[9]); assume_abort_if_not(__startrek_min[9] == __startrek_start[9]); assume_abort_if_not(__startrek_max[9] == __startrek_end[9]); assume_abort_if_not(6 <= __startrek_start[8]); assume_abort_if_not(__startrek_end[8] <= 8); assume_abort_if_not(__startrek_max[8] < __startrek_min[9]); assume_abort_if_not(__startrek_start[8] == __startrek_end[8]); assume_abort_if_not(__startrek_min[8] == __startrek_start[8]); assume_abort_if_not(__startrek_max[8] == __startrek_end[8]); assume_abort_if_not(5 <= __startrek_start[7]); assume_abort_if_not(__startrek_end[7] <= 7); assume_abort_if_not(__startrek_max[7] < __startrek_min[8]); assume_abort_if_not(__startrek_start[7] == __startrek_end[7]); assume_abort_if_not(__startrek_min[7] == __startrek_start[7]); assume_abort_if_not(__startrek_max[7] == __startrek_end[7]); assume_abort_if_not(4 <= __startrek_start[6]); assume_abort_if_not(__startrek_end[6] <= 6); assume_abort_if_not(__startrek_max[6] < __startrek_min[7]); assume_abort_if_not(__startrek_start[6] == __startrek_end[6]); assume_abort_if_not(__startrek_min[6] == __startrek_start[6]); assume_abort_if_not(__startrek_max[6] == __startrek_end[6]); assume_abort_if_not(3 <= __startrek_start[5]); assume_abort_if_not(__startrek_end[5] <= 5); assume_abort_if_not(__startrek_max[5] < __startrek_min[6]); assume_abort_if_not(__startrek_start[5] == __startrek_end[5]); assume_abort_if_not(__startrek_min[5] == __startrek_start[5]); assume_abort_if_not(__startrek_max[5] == __startrek_end[5]); assume_abort_if_not(2 <= __startrek_start[4]); assume_abort_if_not(__startrek_end[4] <= 4); assume_abort_if_not(__startrek_max[4] < __startrek_min[5]); assume_abort_if_not(__startrek_start[4] == __startrek_end[4]); assume_abort_if_not(__startrek_min[4] == __startrek_start[4]); assume_abort_if_not(__startrek_max[4] == __startrek_end[4]); assume_abort_if_not(1 <= __startrek_start[3]); assume_abort_if_not(__startrek_end[3] <= 3); assume_abort_if_not(__startrek_max[3] < __startrek_min[4]); assume_abort_if_not(__startrek_start[3] == __startrek_end[3]); assume_abort_if_not(__startrek_min[3] == __startrek_start[3]); assume_abort_if_not(__startrek_max[3] == __startrek_end[3]); assume_abort_if_not(0 <= __startrek_start[2]); assume_abort_if_not(__startrek_end[2] <= 2); assume_abort_if_not(__startrek_max[2] < __startrek_min[3]); assume_abort_if_not(__startrek_start[2] == __startrek_end[2]); assume_abort_if_not(__startrek_min[2] == __startrek_start[2]); assume_abort_if_not(__startrek_max[2] == __startrek_end[2]); assume_abort_if_not(0 <= __startrek_start[1]); assume_abort_if_not(__startrek_end[1] <= 13); assume_abort_if_not(__startrek_max[1] < __startrek_min[14]); assume_abort_if_not(__startrek_start[1] <= __startrek_end[1]); if (__startrek_start[1] < __startrek_min[2]) { assume_abort_if_not(__startrek_min[1] == __startrek_start[1]); } else { assume_abort_if_not(__startrek_min[1] == __startrek_min[2]); } if (__startrek_end[1] > __startrek_max[13]) { assume_abort_if_not(__startrek_max[1] == __startrek_end[1]); } else { assume_abort_if_not(__startrek_max[1] == __startrek_max[13]); } assume_abort_if_not(0 <= __startrek_start[0]); assume_abort_if_not(__startrek_end[0] <= 26); assume_abort_if_not(__startrek_start[0] <= __startrek_end[0]); if (__startrek_start[0] < __startrek_min[1]) { assume_abort_if_not(__startrek_min[0] == __startrek_start[0]); } else { assume_abort_if_not(__startrek_min[0] == __startrek_min[1]); } if (__startrek_end[0] > __startrek_max[14]) { assume_abort_if_not(__startrek_max[0] == __startrek_end[0]); } else { assume_abort_if_not(__startrek_max[0] == __startrek_max[14]); } assume_abort_if_not(__startrek_end[1] < __startrek_start[0]); assume_abort_if_not(__startrek_end[2] < __startrek_start[1]); assume_abort_if_not(__startrek_end[2] < __startrek_start[0]); assume_abort_if_not(__startrek_end[3] <= __startrek_end[1]); if (__startrek_start[1] <= __startrek_end[3]) { if (__startrek_start[3] <= __startrek_end[1]) { { assume_abort_if_not(__startrek_start[1] <= __startrek_start[3]); assume_abort_if_not(__startrek_end[3] < __startrek_end[1]); } } } assume_abort_if_not(__startrek_end[3] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[3]) { if (__startrek_start[3] <= __startrek_end[0]) { { assume_abort_if_not(__startrek_start[0] <= __startrek_start[3]); assume_abort_if_not(__startrek_end[3] < __startrek_end[0]); } } } assume_abort_if_not(__startrek_end[1] < __startrek_start[4]); assume_abort_if_not(__startrek_end[4] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[4]) { if (__startrek_start[4] <= __startrek_end[0]) { { assume_abort_if_not(__startrek_start[0] <= __startrek_start[4]); assume_abort_if_not(__startrek_end[4] < __startrek_end[0]); } } } assume_abort_if_not(__startrek_end[1] < __startrek_start[5]); assume_abort_if_not(__startrek_end[0] < __startrek_start[5]); assume_abort_if_not(__startrek_end[1] < __startrek_start[6]); assume_abort_if_not(__startrek_end[0] < __startrek_start[6]); assume_abort_if_not(__startrek_end[1] < __startrek_start[7]); assume_abort_if_not(__startrek_end[0] < __startrek_start[7]); assume_abort_if_not(__startrek_end[1] < __startrek_start[8]); assume_abort_if_not(__startrek_end[0] < __startrek_start[8]); assume_abort_if_not(__startrek_end[1] < __startrek_start[9]); assume_abort_if_not(__startrek_end[0] < __startrek_start[9]); assume_abort_if_not(__startrek_end[1] < __startrek_start[10]); assume_abort_if_not(__startrek_end[0] < __startrek_start[10]); assume_abort_if_not(__startrek_end[1] < __startrek_start[11]); assume_abort_if_not(__startrek_end[0] < __startrek_start[11]); assume_abort_if_not(__startrek_end[1] < __startrek_start[12]); assume_abort_if_not(__startrek_end[0] < __startrek_start[12]); assume_abort_if_not(__startrek_end[1] < __startrek_start[13]); assume_abort_if_not(__startrek_end[0] < __startrek_start[13]); assume_abort_if_not(__startrek_end[0] < __startrek_start[14]); assume_abort_if_not(__startrek_end[15] < __startrek_start[14]); assume_abort_if_not(__startrek_end[0] < __startrek_start[15]); assume_abort_if_not(__startrek_end[16] <= __startrek_end[14]); if (__startrek_start[14] <= __startrek_end[16]) { if (__startrek_start[16] <= __startrek_end[14]) { { assume_abort_if_not(__startrek_start[14] <= __startrek_start[16]); assume_abort_if_not(__startrek_end[16] < __startrek_end[14]); } } } assume_abort_if_not(__startrek_end[0] < __startrek_start[16]); assume_abort_if_not(__startrek_end[14] < __startrek_start[17]); assume_abort_if_not(__startrek_end[0] < __startrek_start[17]); assume_abort_if_not(__startrek_end[14] < __startrek_start[18]); assume_abort_if_not(__startrek_end[0] < __startrek_start[18]); assume_abort_if_not(__startrek_end[14] < __startrek_start[19]); assume_abort_if_not(__startrek_end[0] < __startrek_start[19]); assume_abort_if_not(__startrek_end[14] < __startrek_start[20]); assume_abort_if_not(__startrek_end[0] < __startrek_start[20]); assume_abort_if_not(__startrek_end[14] < __startrek_start[21]); assume_abort_if_not(__startrek_end[0] < __startrek_start[21]); assume_abort_if_not(__startrek_end[14] < __startrek_start[22]); assume_abort_if_not(__startrek_end[0] < __startrek_start[22]); assume_abort_if_not(__startrek_end[14] < __startrek_start[23]); assume_abort_if_not(__startrek_end[0] < __startrek_start[23]); assume_abort_if_not(__startrek_end[14] < __startrek_start[24]); assume_abort_if_not(__startrek_end[0] < __startrek_start[24]); assume_abort_if_not(__startrek_end[14] < __startrek_start[25]); assume_abort_if_not(__startrek_end[0] < __startrek_start[25]); assume_abort_if_not(__startrek_end[14] < __startrek_start[26]); assume_abort_if_not(__startrek_end[0] < __startrek_start[26]); } } __inline void __startrek_init_globals(void) { { _i_obstacle_flag_[1] = __VERIFIER_nondet_bool(); _obstacle_flag_[1] = _i_obstacle_flag_[1]; _i_obstacle_flag_[2] = __VERIFIER_nondet_bool(); _obstacle_flag_[2] = _i_obstacle_flag_[2]; _i_obstacle_flag_[3] = __VERIFIER_nondet_bool(); _obstacle_flag_[3] = _i_obstacle_flag_[3]; _i_obstacle_flag_[4] = __VERIFIER_nondet_bool(); _obstacle_flag_[4] = _i_obstacle_flag_[4]; _i_obstacle_flag_[5] = __VERIFIER_nondet_bool(); _obstacle_flag_[5] = _i_obstacle_flag_[5]; _i_obstacle_flag_[6] = __VERIFIER_nondet_bool(); _obstacle_flag_[6] = _i_obstacle_flag_[6]; _i_obstacle_flag_[7] = __VERIFIER_nondet_bool(); _obstacle_flag_[7] = _i_obstacle_flag_[7]; _i_obstacle_flag_[8] = __VERIFIER_nondet_bool(); _obstacle_flag_[8] = _i_obstacle_flag_[8]; _i_obstacle_flag_[9] = __VERIFIER_nondet_bool(); _obstacle_flag_[9] = _i_obstacle_flag_[9]; _i_obstacle_flag_[10] = __VERIFIER_nondet_bool(); _obstacle_flag_[10] = _i_obstacle_flag_[10]; _i_obstacle_flag_[11] = __VERIFIER_nondet_bool(); _obstacle_flag_[11] = _i_obstacle_flag_[11]; _i_obstacle_flag_[12] = __VERIFIER_nondet_bool(); _obstacle_flag_[12] = _i_obstacle_flag_[12]; _i_obstacle_flag_[13] = __VERIFIER_nondet_bool(); _obstacle_flag_[13] = _i_obstacle_flag_[13]; _i_obstacle_flag_[14] = __VERIFIER_nondet_bool(); _obstacle_flag_[14] = _i_obstacle_flag_[14]; _i_obstacle_flag_[15] = __VERIFIER_nondet_bool(); _obstacle_flag_[15] = _i_obstacle_flag_[15]; _i_obstacle_flag_[16] = __VERIFIER_nondet_bool(); _obstacle_flag_[16] = _i_obstacle_flag_[16]; _i_obstacle_flag_[17] = __VERIFIER_nondet_bool(); _obstacle_flag_[17] = _i_obstacle_flag_[17]; _i_obstacle_flag_[18] = __VERIFIER_nondet_bool(); _obstacle_flag_[18] = _i_obstacle_flag_[18]; _i_obstacle_flag_[19] = __VERIFIER_nondet_bool(); _obstacle_flag_[19] = _i_obstacle_flag_[19]; _i_obstacle_flag_[20] = __VERIFIER_nondet_bool(); _obstacle_flag_[20] = _i_obstacle_flag_[20]; _i_obstacle_flag_[21] = __VERIFIER_nondet_bool(); _obstacle_flag_[21] = _i_obstacle_flag_[21]; _i_obstacle_flag_[22] = __VERIFIER_nondet_bool(); _obstacle_flag_[22] = _i_obstacle_flag_[22]; _i_obstacle_flag_[23] = __VERIFIER_nondet_bool(); _obstacle_flag_[23] = _i_obstacle_flag_[23]; _i_obstacle_flag_[24] = __VERIFIER_nondet_bool(); _obstacle_flag_[24] = _i_obstacle_flag_[24]; _i_obstacle_flag_[25] = __VERIFIER_nondet_bool(); _obstacle_flag_[25] = _i_obstacle_flag_[25]; _i_obstacle_flag_[26] = __VERIFIER_nondet_bool(); _obstacle_flag_[26] = _i_obstacle_flag_[26]; _i_nxtway_gs_mode_[1] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[1] = _i_nxtway_gs_mode_[1]; _i_nxtway_gs_mode_[2] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[2] = _i_nxtway_gs_mode_[2]; _i_nxtway_gs_mode_[3] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[3] = _i_nxtway_gs_mode_[3]; _i_nxtway_gs_mode_[4] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[4] = _i_nxtway_gs_mode_[4]; _i_nxtway_gs_mode_[5] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[5] = _i_nxtway_gs_mode_[5]; _i_nxtway_gs_mode_[6] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[6] = _i_nxtway_gs_mode_[6]; _i_nxtway_gs_mode_[7] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[7] = _i_nxtway_gs_mode_[7]; _i_nxtway_gs_mode_[8] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[8] = _i_nxtway_gs_mode_[8]; _i_nxtway_gs_mode_[9] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[9] = _i_nxtway_gs_mode_[9]; _i_nxtway_gs_mode_[10] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[10] = _i_nxtway_gs_mode_[10]; _i_nxtway_gs_mode_[11] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[11] = _i_nxtway_gs_mode_[11]; _i_nxtway_gs_mode_[12] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[12] = _i_nxtway_gs_mode_[12]; _i_nxtway_gs_mode_[13] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[13] = _i_nxtway_gs_mode_[13]; _i_nxtway_gs_mode_[14] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[14] = _i_nxtway_gs_mode_[14]; _i_nxtway_gs_mode_[15] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[15] = _i_nxtway_gs_mode_[15]; _i_nxtway_gs_mode_[16] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[16] = _i_nxtway_gs_mode_[16]; _i_nxtway_gs_mode_[17] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[17] = _i_nxtway_gs_mode_[17]; _i_nxtway_gs_mode_[18] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[18] = _i_nxtway_gs_mode_[18]; _i_nxtway_gs_mode_[19] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[19] = _i_nxtway_gs_mode_[19]; _i_nxtway_gs_mode_[20] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[20] = _i_nxtway_gs_mode_[20]; _i_nxtway_gs_mode_[21] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[21] = _i_nxtway_gs_mode_[21]; _i_nxtway_gs_mode_[22] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[22] = _i_nxtway_gs_mode_[22]; _i_nxtway_gs_mode_[23] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[23] = _i_nxtway_gs_mode_[23]; _i_nxtway_gs_mode_[24] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[24] = _i_nxtway_gs_mode_[24]; _i_nxtway_gs_mode_[25] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[25] = _i_nxtway_gs_mode_[25]; _i_nxtway_gs_mode_[26] = __VERIFIER_nondet_uchar(); _nxtway_gs_mode_[26] = _i_nxtway_gs_mode_[26]; } } __inline static _Bool __startrek_cs_t0(void) { _Bool c1 ; unsigned char o2 ; { if (__startrek_lock) { return (0); } c1 = __VERIFIER_nondet_bool(); if (c1) { return (0); } o2 = __startrek_round; __startrek_round = __VERIFIER_nondet_uchar(); assume_abort_if_not(__startrek_round > o2); assume_abort_if_not(__startrek_round <= __startrek_job_end); if (__startrek_round != __startrek_job_end) { { switch (__startrek_job) { case 0: if (__startrek_start[26] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[26]); } if (__startrek_start[25] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[25]); } if (__startrek_start[24] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[24]); } if (__startrek_start[23] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[23]); } if (__startrek_start[22] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[22]); } if (__startrek_start[21] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[21]); } if (__startrek_start[20] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[20]); } if (__startrek_start[19] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[19]); } if (__startrek_start[18] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[18]); } if (__startrek_start[17] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[17]); } if (__startrek_start[16] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[16]); } if (__startrek_start[15] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[15]); } if (__startrek_start[14] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[14]); } if (__startrek_start[13] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[13]); } if (__startrek_start[12] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[12]); } if (__startrek_start[11] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[11]); } if (__startrek_start[10] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[10]); } if (__startrek_start[9] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[9]); } if (__startrek_start[8] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[8]); } if (__startrek_start[7] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[7]); } if (__startrek_start[6] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[6]); } if (__startrek_start[5] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[5]); } if (__startrek_start[4] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[4]); } if (__startrek_start[3] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[3]); } if (__startrek_start[2] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[2]); } if (__startrek_start[1] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[1]); } break; } } } return (1); } } __inline static _Bool __startrek_cs_t1(void) { _Bool c1 ; unsigned char o2 ; { if (__startrek_lock) { return (0); } c1 = __VERIFIER_nondet_bool(); if (c1) { return (0); } o2 = __startrek_round; __startrek_round = __VERIFIER_nondet_uchar(); assume_abort_if_not(__startrek_round > o2); assume_abort_if_not(__startrek_round <= __startrek_job_end); if (__startrek_round != __startrek_job_end) { { switch (__startrek_job) { case 14: if (__startrek_start[26] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[26]); } if (__startrek_start[25] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[25]); } if (__startrek_start[24] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[24]); } if (__startrek_start[23] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[23]); } if (__startrek_start[22] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[22]); } if (__startrek_start[21] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[21]); } if (__startrek_start[20] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[20]); } if (__startrek_start[19] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[19]); } if (__startrek_start[18] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[18]); } if (__startrek_start[17] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[17]); } if (__startrek_start[16] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[16]); } if (__startrek_start[15] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[15]); } break; case 1: if (__startrek_start[13] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[13]); } if (__startrek_start[12] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[12]); } if (__startrek_start[11] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[11]); } if (__startrek_start[10] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[10]); } if (__startrek_start[9] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[9]); } if (__startrek_start[8] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[8]); } if (__startrek_start[7] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[7]); } if (__startrek_start[6] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[6]); } if (__startrek_start[5] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[5]); } if (__startrek_start[4] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[4]); } if (__startrek_start[3] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[3]); } if (__startrek_start[2] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end[2]); } break; } } } return (1); } } __inline static _Bool __startrek_cs_t2(void) { { return (0); } } __inline void __startrek_user_init(void) { { } } void __startrek_hyperperiod(void) { { __startrek_schedule_jobs(); __startrek_init_globals(); __startrek_round = __startrek_start[2]; __startrek_task = 2; __startrek_job_end = __startrek_end[2]; __startrek_job = 2; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 0: assume_abort_if_not(_obstacle_flag_[0] == _i_obstacle_flag_[1]); assume_abort_if_not(_nxtway_gs_mode_[0] == _i_nxtway_gs_mode_[1]); break; case 1: assume_abort_if_not(_obstacle_flag_[1] == _i_obstacle_flag_[2]); assume_abort_if_not(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); break; case 2: assume_abort_if_not(_obstacle_flag_[2] == _i_obstacle_flag_[3]); assume_abort_if_not(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); break; } __startrek_round = __startrek_start[1]; __startrek_task = 1; __startrek_job_end = __startrek_end[1]; __startrek_job = 1; __startrek_entry_pt_OSEK_Task_ts2(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 0: assume_abort_if_not(_obstacle_flag_[0] == _i_obstacle_flag_[1]); assume_abort_if_not(_nxtway_gs_mode_[0] == _i_nxtway_gs_mode_[1]); break; case 1: assume_abort_if_not(_obstacle_flag_[1] == _i_obstacle_flag_[2]); assume_abort_if_not(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); break; case 2: assume_abort_if_not(_obstacle_flag_[2] == _i_obstacle_flag_[3]); assume_abort_if_not(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); break; case 3: assume_abort_if_not(_obstacle_flag_[3] == _i_obstacle_flag_[4]); assume_abort_if_not(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); break; case 4: assume_abort_if_not(_obstacle_flag_[4] == _i_obstacle_flag_[5]); assume_abort_if_not(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); break; case 5: assume_abort_if_not(_obstacle_flag_[5] == _i_obstacle_flag_[6]); assume_abort_if_not(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); break; case 6: assume_abort_if_not(_obstacle_flag_[6] == _i_obstacle_flag_[7]); assume_abort_if_not(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); break; case 7: assume_abort_if_not(_obstacle_flag_[7] == _i_obstacle_flag_[8]); assume_abort_if_not(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); break; case 8: assume_abort_if_not(_obstacle_flag_[8] == _i_obstacle_flag_[9]); assume_abort_if_not(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); break; case 9: assume_abort_if_not(_obstacle_flag_[9] == _i_obstacle_flag_[10]); assume_abort_if_not(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); break; case 10: assume_abort_if_not(_obstacle_flag_[10] == _i_obstacle_flag_[11]); assume_abort_if_not(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); break; case 11: assume_abort_if_not(_obstacle_flag_[11] == _i_obstacle_flag_[12]); assume_abort_if_not(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); break; case 12: assume_abort_if_not(_obstacle_flag_[12] == _i_obstacle_flag_[13]); assume_abort_if_not(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); break; case 13: assume_abort_if_not(_obstacle_flag_[13] == _i_obstacle_flag_[14]); assume_abort_if_not(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); break; } __startrek_round = __startrek_start[0]; __startrek_task = 0; __startrek_job_end = __startrek_end[0]; __startrek_job = 0; __startrek_entry_pt_OSEK_Task_Background(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 0: assume_abort_if_not(_obstacle_flag_[0] == _i_obstacle_flag_[1]); assume_abort_if_not(_nxtway_gs_mode_[0] == _i_nxtway_gs_mode_[1]); break; case 1: assume_abort_if_not(_obstacle_flag_[1] == _i_obstacle_flag_[2]); assume_abort_if_not(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); break; case 2: assume_abort_if_not(_obstacle_flag_[2] == _i_obstacle_flag_[3]); assume_abort_if_not(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); break; case 3: assume_abort_if_not(_obstacle_flag_[3] == _i_obstacle_flag_[4]); assume_abort_if_not(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); break; case 4: assume_abort_if_not(_obstacle_flag_[4] == _i_obstacle_flag_[5]); assume_abort_if_not(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); break; case 5: assume_abort_if_not(_obstacle_flag_[5] == _i_obstacle_flag_[6]); assume_abort_if_not(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); break; case 6: assume_abort_if_not(_obstacle_flag_[6] == _i_obstacle_flag_[7]); assume_abort_if_not(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); break; case 7: assume_abort_if_not(_obstacle_flag_[7] == _i_obstacle_flag_[8]); assume_abort_if_not(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); break; case 8: assume_abort_if_not(_obstacle_flag_[8] == _i_obstacle_flag_[9]); assume_abort_if_not(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); break; case 9: assume_abort_if_not(_obstacle_flag_[9] == _i_obstacle_flag_[10]); assume_abort_if_not(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); break; case 10: assume_abort_if_not(_obstacle_flag_[10] == _i_obstacle_flag_[11]); assume_abort_if_not(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); break; case 11: assume_abort_if_not(_obstacle_flag_[11] == _i_obstacle_flag_[12]); assume_abort_if_not(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); break; case 12: assume_abort_if_not(_obstacle_flag_[12] == _i_obstacle_flag_[13]); assume_abort_if_not(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); break; case 13: assume_abort_if_not(_obstacle_flag_[13] == _i_obstacle_flag_[14]); assume_abort_if_not(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); break; case 14: assume_abort_if_not(_obstacle_flag_[14] == _i_obstacle_flag_[15]); assume_abort_if_not(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); break; case 15: assume_abort_if_not(_obstacle_flag_[15] == _i_obstacle_flag_[16]); assume_abort_if_not(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); break; case 16: assume_abort_if_not(_obstacle_flag_[16] == _i_obstacle_flag_[17]); assume_abort_if_not(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); break; case 17: assume_abort_if_not(_obstacle_flag_[17] == _i_obstacle_flag_[18]); assume_abort_if_not(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); break; case 18: assume_abort_if_not(_obstacle_flag_[18] == _i_obstacle_flag_[19]); assume_abort_if_not(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); break; case 19: assume_abort_if_not(_obstacle_flag_[19] == _i_obstacle_flag_[20]); assume_abort_if_not(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); break; case 20: assume_abort_if_not(_obstacle_flag_[20] == _i_obstacle_flag_[21]); assume_abort_if_not(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); break; case 21: assume_abort_if_not(_obstacle_flag_[21] == _i_obstacle_flag_[22]); assume_abort_if_not(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); break; case 22: assume_abort_if_not(_obstacle_flag_[22] == _i_obstacle_flag_[23]); assume_abort_if_not(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); break; case 23: assume_abort_if_not(_obstacle_flag_[23] == _i_obstacle_flag_[24]); assume_abort_if_not(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); break; case 24: assume_abort_if_not(_obstacle_flag_[24] == _i_obstacle_flag_[25]); assume_abort_if_not(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); break; case 25: assume_abort_if_not(_obstacle_flag_[25] == _i_obstacle_flag_[26]); assume_abort_if_not(_nxtway_gs_mode_[25] == _i_nxtway_gs_mode_[26]); break; } __startrek_round = __startrek_start[3]; __startrek_task = 2; __startrek_job_end = __startrek_end[3]; __startrek_job = 3; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 1: assume_abort_if_not(_obstacle_flag_[1] == _i_obstacle_flag_[2]); assume_abort_if_not(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); break; case 2: assume_abort_if_not(_obstacle_flag_[2] == _i_obstacle_flag_[3]); assume_abort_if_not(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); break; case 3: assume_abort_if_not(_obstacle_flag_[3] == _i_obstacle_flag_[4]); assume_abort_if_not(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); break; } __startrek_round = __startrek_start[4]; __startrek_task = 2; __startrek_job_end = __startrek_end[4]; __startrek_job = 4; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 2: assume_abort_if_not(_obstacle_flag_[2] == _i_obstacle_flag_[3]); assume_abort_if_not(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); break; case 3: assume_abort_if_not(_obstacle_flag_[3] == _i_obstacle_flag_[4]); assume_abort_if_not(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); break; case 4: assume_abort_if_not(_obstacle_flag_[4] == _i_obstacle_flag_[5]); assume_abort_if_not(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); break; } __startrek_round = __startrek_start[5]; __startrek_task = 2; __startrek_job_end = __startrek_end[5]; __startrek_job = 5; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 3: assume_abort_if_not(_obstacle_flag_[3] == _i_obstacle_flag_[4]); assume_abort_if_not(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); break; case 4: assume_abort_if_not(_obstacle_flag_[4] == _i_obstacle_flag_[5]); assume_abort_if_not(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); break; case 5: assume_abort_if_not(_obstacle_flag_[5] == _i_obstacle_flag_[6]); assume_abort_if_not(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); break; } __startrek_round = __startrek_start[6]; __startrek_task = 2; __startrek_job_end = __startrek_end[6]; __startrek_job = 6; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 4: assume_abort_if_not(_obstacle_flag_[4] == _i_obstacle_flag_[5]); assume_abort_if_not(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); break; case 5: assume_abort_if_not(_obstacle_flag_[5] == _i_obstacle_flag_[6]); assume_abort_if_not(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); break; case 6: assume_abort_if_not(_obstacle_flag_[6] == _i_obstacle_flag_[7]); assume_abort_if_not(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); break; } __startrek_round = __startrek_start[7]; __startrek_task = 2; __startrek_job_end = __startrek_end[7]; __startrek_job = 7; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 5: assume_abort_if_not(_obstacle_flag_[5] == _i_obstacle_flag_[6]); assume_abort_if_not(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); break; case 6: assume_abort_if_not(_obstacle_flag_[6] == _i_obstacle_flag_[7]); assume_abort_if_not(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); break; case 7: assume_abort_if_not(_obstacle_flag_[7] == _i_obstacle_flag_[8]); assume_abort_if_not(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); break; } __startrek_round = __startrek_start[8]; __startrek_task = 2; __startrek_job_end = __startrek_end[8]; __startrek_job = 8; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 6: assume_abort_if_not(_obstacle_flag_[6] == _i_obstacle_flag_[7]); assume_abort_if_not(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); break; case 7: assume_abort_if_not(_obstacle_flag_[7] == _i_obstacle_flag_[8]); assume_abort_if_not(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); break; case 8: assume_abort_if_not(_obstacle_flag_[8] == _i_obstacle_flag_[9]); assume_abort_if_not(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); break; } __startrek_round = __startrek_start[9]; __startrek_task = 2; __startrek_job_end = __startrek_end[9]; __startrek_job = 9; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 7: assume_abort_if_not(_obstacle_flag_[7] == _i_obstacle_flag_[8]); assume_abort_if_not(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); break; case 8: assume_abort_if_not(_obstacle_flag_[8] == _i_obstacle_flag_[9]); assume_abort_if_not(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); break; case 9: assume_abort_if_not(_obstacle_flag_[9] == _i_obstacle_flag_[10]); assume_abort_if_not(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); break; } __startrek_round = __startrek_start[10]; __startrek_task = 2; __startrek_job_end = __startrek_end[10]; __startrek_job = 10; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 8: assume_abort_if_not(_obstacle_flag_[8] == _i_obstacle_flag_[9]); assume_abort_if_not(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); break; case 9: assume_abort_if_not(_obstacle_flag_[9] == _i_obstacle_flag_[10]); assume_abort_if_not(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); break; case 10: assume_abort_if_not(_obstacle_flag_[10] == _i_obstacle_flag_[11]); assume_abort_if_not(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); break; } __startrek_round = __startrek_start[11]; __startrek_task = 2; __startrek_job_end = __startrek_end[11]; __startrek_job = 11; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 9: assume_abort_if_not(_obstacle_flag_[9] == _i_obstacle_flag_[10]); assume_abort_if_not(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); break; case 10: assume_abort_if_not(_obstacle_flag_[10] == _i_obstacle_flag_[11]); assume_abort_if_not(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); break; case 11: assume_abort_if_not(_obstacle_flag_[11] == _i_obstacle_flag_[12]); assume_abort_if_not(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); break; } __startrek_round = __startrek_start[12]; __startrek_task = 2; __startrek_job_end = __startrek_end[12]; __startrek_job = 12; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 10: assume_abort_if_not(_obstacle_flag_[10] == _i_obstacle_flag_[11]); assume_abort_if_not(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); break; case 11: assume_abort_if_not(_obstacle_flag_[11] == _i_obstacle_flag_[12]); assume_abort_if_not(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); break; case 12: assume_abort_if_not(_obstacle_flag_[12] == _i_obstacle_flag_[13]); assume_abort_if_not(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); break; } __startrek_round = __startrek_start[13]; __startrek_task = 2; __startrek_job_end = __startrek_end[13]; __startrek_job = 13; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 11: assume_abort_if_not(_obstacle_flag_[11] == _i_obstacle_flag_[12]); assume_abort_if_not(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); break; case 12: assume_abort_if_not(_obstacle_flag_[12] == _i_obstacle_flag_[13]); assume_abort_if_not(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); break; case 13: assume_abort_if_not(_obstacle_flag_[13] == _i_obstacle_flag_[14]); assume_abort_if_not(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); break; } __startrek_round = __startrek_start[15]; __startrek_task = 2; __startrek_job_end = __startrek_end[15]; __startrek_job = 15; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 13: assume_abort_if_not(_obstacle_flag_[13] == _i_obstacle_flag_[14]); assume_abort_if_not(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); break; case 14: assume_abort_if_not(_obstacle_flag_[14] == _i_obstacle_flag_[15]); assume_abort_if_not(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); break; case 15: assume_abort_if_not(_obstacle_flag_[15] == _i_obstacle_flag_[16]); assume_abort_if_not(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); break; } __startrek_round = __startrek_start[14]; __startrek_task = 1; __startrek_job_end = __startrek_end[14]; __startrek_job = 14; __startrek_entry_pt_OSEK_Task_ts2(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 13: assume_abort_if_not(_obstacle_flag_[13] == _i_obstacle_flag_[14]); assume_abort_if_not(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); break; case 14: assume_abort_if_not(_obstacle_flag_[14] == _i_obstacle_flag_[15]); assume_abort_if_not(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); break; case 15: assume_abort_if_not(_obstacle_flag_[15] == _i_obstacle_flag_[16]); assume_abort_if_not(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); break; case 16: assume_abort_if_not(_obstacle_flag_[16] == _i_obstacle_flag_[17]); assume_abort_if_not(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); break; case 17: assume_abort_if_not(_obstacle_flag_[17] == _i_obstacle_flag_[18]); assume_abort_if_not(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); break; case 18: assume_abort_if_not(_obstacle_flag_[18] == _i_obstacle_flag_[19]); assume_abort_if_not(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); break; case 19: assume_abort_if_not(_obstacle_flag_[19] == _i_obstacle_flag_[20]); assume_abort_if_not(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); break; case 20: assume_abort_if_not(_obstacle_flag_[20] == _i_obstacle_flag_[21]); assume_abort_if_not(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); break; case 21: assume_abort_if_not(_obstacle_flag_[21] == _i_obstacle_flag_[22]); assume_abort_if_not(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); break; case 22: assume_abort_if_not(_obstacle_flag_[22] == _i_obstacle_flag_[23]); assume_abort_if_not(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); break; case 23: assume_abort_if_not(_obstacle_flag_[23] == _i_obstacle_flag_[24]); assume_abort_if_not(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); break; case 24: assume_abort_if_not(_obstacle_flag_[24] == _i_obstacle_flag_[25]); assume_abort_if_not(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); break; case 25: assume_abort_if_not(_obstacle_flag_[25] == _i_obstacle_flag_[26]); assume_abort_if_not(_nxtway_gs_mode_[25] == _i_nxtway_gs_mode_[26]); break; } __startrek_round = __startrek_start[16]; __startrek_task = 2; __startrek_job_end = __startrek_end[16]; __startrek_job = 16; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 14: assume_abort_if_not(_obstacle_flag_[14] == _i_obstacle_flag_[15]); assume_abort_if_not(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); break; case 15: assume_abort_if_not(_obstacle_flag_[15] == _i_obstacle_flag_[16]); assume_abort_if_not(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); break; case 16: assume_abort_if_not(_obstacle_flag_[16] == _i_obstacle_flag_[17]); assume_abort_if_not(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); break; } __startrek_round = __startrek_start[17]; __startrek_task = 2; __startrek_job_end = __startrek_end[17]; __startrek_job = 17; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 15: assume_abort_if_not(_obstacle_flag_[15] == _i_obstacle_flag_[16]); assume_abort_if_not(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); break; case 16: assume_abort_if_not(_obstacle_flag_[16] == _i_obstacle_flag_[17]); assume_abort_if_not(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); break; case 17: assume_abort_if_not(_obstacle_flag_[17] == _i_obstacle_flag_[18]); assume_abort_if_not(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); break; } __startrek_round = __startrek_start[18]; __startrek_task = 2; __startrek_job_end = __startrek_end[18]; __startrek_job = 18; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 16: assume_abort_if_not(_obstacle_flag_[16] == _i_obstacle_flag_[17]); assume_abort_if_not(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); break; case 17: assume_abort_if_not(_obstacle_flag_[17] == _i_obstacle_flag_[18]); assume_abort_if_not(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); break; case 18: assume_abort_if_not(_obstacle_flag_[18] == _i_obstacle_flag_[19]); assume_abort_if_not(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); break; } __startrek_round = __startrek_start[19]; __startrek_task = 2; __startrek_job_end = __startrek_end[19]; __startrek_job = 19; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 17: assume_abort_if_not(_obstacle_flag_[17] == _i_obstacle_flag_[18]); assume_abort_if_not(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); break; case 18: assume_abort_if_not(_obstacle_flag_[18] == _i_obstacle_flag_[19]); assume_abort_if_not(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); break; case 19: assume_abort_if_not(_obstacle_flag_[19] == _i_obstacle_flag_[20]); assume_abort_if_not(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); break; } __startrek_round = __startrek_start[20]; __startrek_task = 2; __startrek_job_end = __startrek_end[20]; __startrek_job = 20; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 18: assume_abort_if_not(_obstacle_flag_[18] == _i_obstacle_flag_[19]); assume_abort_if_not(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); break; case 19: assume_abort_if_not(_obstacle_flag_[19] == _i_obstacle_flag_[20]); assume_abort_if_not(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); break; case 20: assume_abort_if_not(_obstacle_flag_[20] == _i_obstacle_flag_[21]); assume_abort_if_not(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); break; } __startrek_round = __startrek_start[21]; __startrek_task = 2; __startrek_job_end = __startrek_end[21]; __startrek_job = 21; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 19: assume_abort_if_not(_obstacle_flag_[19] == _i_obstacle_flag_[20]); assume_abort_if_not(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); break; case 20: assume_abort_if_not(_obstacle_flag_[20] == _i_obstacle_flag_[21]); assume_abort_if_not(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); break; case 21: assume_abort_if_not(_obstacle_flag_[21] == _i_obstacle_flag_[22]); assume_abort_if_not(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); break; } __startrek_round = __startrek_start[22]; __startrek_task = 2; __startrek_job_end = __startrek_end[22]; __startrek_job = 22; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 20: assume_abort_if_not(_obstacle_flag_[20] == _i_obstacle_flag_[21]); assume_abort_if_not(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); break; case 21: assume_abort_if_not(_obstacle_flag_[21] == _i_obstacle_flag_[22]); assume_abort_if_not(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); break; case 22: assume_abort_if_not(_obstacle_flag_[22] == _i_obstacle_flag_[23]); assume_abort_if_not(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); break; } __startrek_round = __startrek_start[23]; __startrek_task = 2; __startrek_job_end = __startrek_end[23]; __startrek_job = 23; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 21: assume_abort_if_not(_obstacle_flag_[21] == _i_obstacle_flag_[22]); assume_abort_if_not(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); break; case 22: assume_abort_if_not(_obstacle_flag_[22] == _i_obstacle_flag_[23]); assume_abort_if_not(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); break; case 23: assume_abort_if_not(_obstacle_flag_[23] == _i_obstacle_flag_[24]); assume_abort_if_not(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); break; } __startrek_round = __startrek_start[24]; __startrek_task = 2; __startrek_job_end = __startrek_end[24]; __startrek_job = 24; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 22: assume_abort_if_not(_obstacle_flag_[22] == _i_obstacle_flag_[23]); assume_abort_if_not(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); break; case 23: assume_abort_if_not(_obstacle_flag_[23] == _i_obstacle_flag_[24]); assume_abort_if_not(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); break; case 24: assume_abort_if_not(_obstacle_flag_[24] == _i_obstacle_flag_[25]); assume_abort_if_not(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); break; } __startrek_round = __startrek_start[25]; __startrek_task = 2; __startrek_job_end = __startrek_end[25]; __startrek_job = 25; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 23: assume_abort_if_not(_obstacle_flag_[23] == _i_obstacle_flag_[24]); assume_abort_if_not(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); break; case 24: assume_abort_if_not(_obstacle_flag_[24] == _i_obstacle_flag_[25]); assume_abort_if_not(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); break; case 25: assume_abort_if_not(_obstacle_flag_[25] == _i_obstacle_flag_[26]); assume_abort_if_not(_nxtway_gs_mode_[25] == _i_nxtway_gs_mode_[26]); break; } __startrek_round = __startrek_start[26]; __startrek_task = 2; __startrek_job_end = __startrek_end[26]; __startrek_job = 26; __startrek_entry_pt_OSEK_Task_ts1(); assume_abort_if_not(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 24: assume_abort_if_not(_obstacle_flag_[24] == _i_obstacle_flag_[25]); assume_abort_if_not(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); break; case 25: assume_abort_if_not(_obstacle_flag_[25] == _i_obstacle_flag_[26]); assume_abort_if_not(_nxtway_gs_mode_[25] == _i_nxtway_gs_mode_[26]); break; } } } int main(void) { { __startrek_init_shared(); __startrek_user_init(); __startrek_hyper_period = 0; __startrek_hyperperiod(); __startrek_user_final(); } return 0; } __inline static unsigned char __startrek_read_nxtway_gs_mode(void) { unsigned char r1 ; _Bool c2 ; unsigned char or3 ; { switch (__startrek_task) { case 0: { or3 = __startrek_round; c2 = __startrek_cs_t0(); { } } break; case 1: { or3 = __startrek_round; c2 = __startrek_cs_t1(); { } } break; case 2: { or3 = __startrek_round; c2 = __startrek_cs_t2(); { } } break; } r1 = _nxtway_gs_mode_[__startrek_round]; return (r1); } } __inline static _Bool __startrek_read_obstacle_flag(void) { _Bool r1 ; _Bool c2 ; unsigned char or3 ; { switch (__startrek_task) { case 0: { or3 = __startrek_round; c2 = __startrek_cs_t0(); { } } break; case 1: { or3 = __startrek_round; c2 = __startrek_cs_t1(); { } } break; case 2: { or3 = __startrek_round; c2 = __startrek_cs_t2(); { } } break; } r1 = _obstacle_flag_[__startrek_round]; return (r1); } } __inline static void __startrek_write_nxtway_gs_mode(unsigned char arg ) { _Bool c2 ; unsigned char or3 ; { switch (__startrek_task) { case 0: { or3 = __startrek_round; c2 = __startrek_cs_t0(); { } } break; case 1: { or3 = __startrek_round; c2 = __startrek_cs_t1(); { } } break; case 2: { or3 = __startrek_round; c2 = __startrek_cs_t2(); { } } break; } _nxtway_gs_mode_[__startrek_round] = arg; } } __inline static void __startrek_write_obstacle_flag(_Bool arg ) { _Bool c2 ; unsigned char or3 ; { switch (__startrek_task) { case 0: { or3 = __startrek_round; c2 = __startrek_cs_t0(); { } } break; case 1: { or3 = __startrek_round; c2 = __startrek_cs_t1(); { } } break; case 2: { or3 = __startrek_round; c2 = __startrek_cs_t2(); { } } break; } _obstacle_flag_[__startrek_round] = arg; } } __inline void __startrek_init_shared(void) { { _obstacle_flag_[0] = __startrek_hidden_obstacle_flag; _nxtway_gs_mode_[0] = __startrek_hidden_nxtway_gs_mode; } } void ecrobot_bt_data_logger(char arg0, char arg1) { return; } void ecrobot_sound_tone(unsigned int arg0, unsigned int arg1, char arg2) { return; } void ecrobot_status_monitor(char *arg0) { return; } void nxt_motor_set_count(unsigned char arg0, char arg1) { return; } void nxt_motor_set_speed(unsigned char arg0, char arg1, char arg2) { return; } void write_mode_on_lcd(unsigned char arg0) { return; }