extern void __VERIFIER_error() __attribute__ ((__noreturn__)); /********************************************************************** Copyright (c) 2013 Carnegie Mellon University. All Rights Reserved. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following acknowledgments and disclaimers. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The names "Carnegie Mellon University," "SEI" and/or "Software Engineering Institute" shall not be used to endorse or promote products derived from this software without prior written permission. For written permission, please contact permission@sei.cmu.edu. 4. Products derived from this software may not be called "SEI" nor may "SEI" appear in their names without prior written permission of permission@sei.cmu.edu. 5. Redistributions of any form whatsoever must retain the following acknowledgment: This material is based upon work funded and supported by the Department of Defense under Contract No. FA8721-05-C-0003 with Carnegie Mellon University for the operation of the Software Engineering Institute, a federally funded research and development center. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the United States Department of Defense. NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING INSTITUTE MATERIAL IS FURNISHEDON AN "AS-IS" BASIS. CARNEGIE MELLON UNIVERSITY MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT, TRADEMARK, OR COPYRIGHT INFRINGEMENT. This material has been approved for public release and unlimited distribution. DM-0000575 **********************************************************************/ /* Generated by CIL v. 1.4.0 */ /* print_CIL_Input is true */ _Bool __startrek_Assert_t2_i0 = 1; _Bool __startrek_Assert_t1_i0 = 1; _Bool __startrek_Assert_t0_i0 = 1; 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 void __startrek_assert_i0(_Bool arg ) ; __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 __VERIFIER_assume(int arg ) ; 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.ok3.i","-S") extern void __startrek_cpu_lock(void) ; extern void __startrek_cpu_unlock(void) ; void assert(_Bool arg) { if (!arg) { ERROR: __VERIFIER_error();} } 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 ++; 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_U32() ; extern char __VERIFIER_nondet_S8() ; 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; __inline static _Bool __startrek_read_observer_obstacle_flag(void) ; __inline static void __startrek_write_observer_obstacle_flag(_Bool arg ) ; _Bool _observer_obstacle_flag_[27] ; _Bool _i_observer_obstacle_flag_[27] ; _Bool __startrek_hidden_observer_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_S8(); 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_U32(); 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_U32(); 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 ; _Bool tmp___3 ; _Bool tmp___4 ; unsigned int tmp___5 ; char tmp___6 ; char tmp___7 ; unsigned int tmp___8 ; { 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) { 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___3 = __startrek_read_observer_obstacle_flag(); if (tmp___3) { tmp___2 = __startrek_read_obstacle_flag(); __startrek_assert_i0(tmp___2); } tmp___4 = __startrek_read_obstacle_flag(); if (tmp___4) { cmd_forward = -100; cmd_turn = 0; } tmp___5 = ecrobot_get_battery_voltage(); tmp___6 = nxt_motor_get_count(1); tmp___7 = nxt_motor_get_count(0); tmp___8 = ecrobot_get_gyro_sensor(3); balance_control((unsigned int )cmd_forward, (unsigned int )cmd_turn, tmp___8, gyro_offset, (unsigned int )tmp___7, (unsigned int )tmp___6, tmp___5, & 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_lock = 1; __startrek_write_observer_obstacle_flag(0); __startrek_lock = 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_lock = 1; __startrek_write_observer_obstacle_flag(1); __startrek_write_obstacle_flag(1); __startrek_lock = 0; } } 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 = 384; __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(); __VERIFIER_assume(24 <= __startrek_start[26]); __VERIFIER_assume(__startrek_end[26] <= 26); __VERIFIER_assume(__startrek_start[26] == __startrek_end[26]); __VERIFIER_assume(__startrek_min[26] == __startrek_start[26]); __VERIFIER_assume(__startrek_max[26] == __startrek_end[26]); __VERIFIER_assume(23 <= __startrek_start[25]); __VERIFIER_assume(__startrek_end[25] <= 25); __VERIFIER_assume(__startrek_max[25] < __startrek_min[26]); __VERIFIER_assume(__startrek_start[25] == __startrek_end[25]); __VERIFIER_assume(__startrek_min[25] == __startrek_start[25]); __VERIFIER_assume(__startrek_max[25] == __startrek_end[25]); __VERIFIER_assume(22 <= __startrek_start[24]); __VERIFIER_assume(__startrek_end[24] <= 24); __VERIFIER_assume(__startrek_max[24] < __startrek_min[25]); __VERIFIER_assume(__startrek_start[24] == __startrek_end[24]); __VERIFIER_assume(__startrek_min[24] == __startrek_start[24]); __VERIFIER_assume(__startrek_max[24] == __startrek_end[24]); __VERIFIER_assume(21 <= __startrek_start[23]); __VERIFIER_assume(__startrek_end[23] <= 23); __VERIFIER_assume(__startrek_max[23] < __startrek_min[24]); __VERIFIER_assume(__startrek_start[23] == __startrek_end[23]); __VERIFIER_assume(__startrek_min[23] == __startrek_start[23]); __VERIFIER_assume(__startrek_max[23] == __startrek_end[23]); __VERIFIER_assume(20 <= __startrek_start[22]); __VERIFIER_assume(__startrek_end[22] <= 22); __VERIFIER_assume(__startrek_max[22] < __startrek_min[23]); __VERIFIER_assume(__startrek_start[22] == __startrek_end[22]); __VERIFIER_assume(__startrek_min[22] == __startrek_start[22]); __VERIFIER_assume(__startrek_max[22] == __startrek_end[22]); __VERIFIER_assume(19 <= __startrek_start[21]); __VERIFIER_assume(__startrek_end[21] <= 21); __VERIFIER_assume(__startrek_max[21] < __startrek_min[22]); __VERIFIER_assume(__startrek_start[21] == __startrek_end[21]); __VERIFIER_assume(__startrek_min[21] == __startrek_start[21]); __VERIFIER_assume(__startrek_max[21] == __startrek_end[21]); __VERIFIER_assume(18 <= __startrek_start[20]); __VERIFIER_assume(__startrek_end[20] <= 20); __VERIFIER_assume(__startrek_max[20] < __startrek_min[21]); __VERIFIER_assume(__startrek_start[20] == __startrek_end[20]); __VERIFIER_assume(__startrek_min[20] == __startrek_start[20]); __VERIFIER_assume(__startrek_max[20] == __startrek_end[20]); __VERIFIER_assume(17 <= __startrek_start[19]); __VERIFIER_assume(__startrek_end[19] <= 19); __VERIFIER_assume(__startrek_max[19] < __startrek_min[20]); __VERIFIER_assume(__startrek_start[19] == __startrek_end[19]); __VERIFIER_assume(__startrek_min[19] == __startrek_start[19]); __VERIFIER_assume(__startrek_max[19] == __startrek_end[19]); __VERIFIER_assume(16 <= __startrek_start[18]); __VERIFIER_assume(__startrek_end[18] <= 18); __VERIFIER_assume(__startrek_max[18] < __startrek_min[19]); __VERIFIER_assume(__startrek_start[18] == __startrek_end[18]); __VERIFIER_assume(__startrek_min[18] == __startrek_start[18]); __VERIFIER_assume(__startrek_max[18] == __startrek_end[18]); __VERIFIER_assume(15 <= __startrek_start[17]); __VERIFIER_assume(__startrek_end[17] <= 17); __VERIFIER_assume(__startrek_max[17] < __startrek_min[18]); __VERIFIER_assume(__startrek_start[17] == __startrek_end[17]); __VERIFIER_assume(__startrek_min[17] == __startrek_start[17]); __VERIFIER_assume(__startrek_max[17] == __startrek_end[17]); __VERIFIER_assume(14 <= __startrek_start[16]); __VERIFIER_assume(__startrek_end[16] <= 16); __VERIFIER_assume(__startrek_max[16] < __startrek_min[17]); __VERIFIER_assume(__startrek_start[16] == __startrek_end[16]); __VERIFIER_assume(__startrek_min[16] == __startrek_start[16]); __VERIFIER_assume(__startrek_max[16] == __startrek_end[16]); __VERIFIER_assume(13 <= __startrek_start[15]); __VERIFIER_assume(__startrek_end[15] <= 15); __VERIFIER_assume(__startrek_max[15] < __startrek_min[16]); __VERIFIER_assume(__startrek_start[15] == __startrek_end[15]); __VERIFIER_assume(__startrek_min[15] == __startrek_start[15]); __VERIFIER_assume(__startrek_max[15] == __startrek_end[15]); __VERIFIER_assume(13 <= __startrek_start[14]); __VERIFIER_assume(__startrek_end[14] <= 26); __VERIFIER_assume(__startrek_start[14] <= __startrek_end[14]); if (__startrek_start[14] < __startrek_min[15]) { __VERIFIER_assume(__startrek_min[14] == __startrek_start[14]); } else { __VERIFIER_assume(__startrek_min[14] == __startrek_min[15]); } if (__startrek_end[14] > __startrek_max[26]) { __VERIFIER_assume(__startrek_max[14] == __startrek_end[14]); } else { __VERIFIER_assume(__startrek_max[14] == __startrek_max[26]); } __VERIFIER_assume(11 <= __startrek_start[13]); __VERIFIER_assume(__startrek_end[13] <= 13); __VERIFIER_assume(__startrek_start[13] == __startrek_end[13]); __VERIFIER_assume(__startrek_min[13] == __startrek_start[13]); __VERIFIER_assume(__startrek_max[13] == __startrek_end[13]); __VERIFIER_assume(10 <= __startrek_start[12]); __VERIFIER_assume(__startrek_end[12] <= 12); __VERIFIER_assume(__startrek_max[12] < __startrek_min[13]); __VERIFIER_assume(__startrek_start[12] == __startrek_end[12]); __VERIFIER_assume(__startrek_min[12] == __startrek_start[12]); __VERIFIER_assume(__startrek_max[12] == __startrek_end[12]); __VERIFIER_assume(9 <= __startrek_start[11]); __VERIFIER_assume(__startrek_end[11] <= 11); __VERIFIER_assume(__startrek_max[11] < __startrek_min[12]); __VERIFIER_assume(__startrek_start[11] == __startrek_end[11]); __VERIFIER_assume(__startrek_min[11] == __startrek_start[11]); __VERIFIER_assume(__startrek_max[11] == __startrek_end[11]); __VERIFIER_assume(8 <= __startrek_start[10]); __VERIFIER_assume(__startrek_end[10] <= 10); __VERIFIER_assume(__startrek_max[10] < __startrek_min[11]); __VERIFIER_assume(__startrek_start[10] == __startrek_end[10]); __VERIFIER_assume(__startrek_min[10] == __startrek_start[10]); __VERIFIER_assume(__startrek_max[10] == __startrek_end[10]); __VERIFIER_assume(7 <= __startrek_start[9]); __VERIFIER_assume(__startrek_end[9] <= 9); __VERIFIER_assume(__startrek_max[9] < __startrek_min[10]); __VERIFIER_assume(__startrek_start[9] == __startrek_end[9]); __VERIFIER_assume(__startrek_min[9] == __startrek_start[9]); __VERIFIER_assume(__startrek_max[9] == __startrek_end[9]); __VERIFIER_assume(6 <= __startrek_start[8]); __VERIFIER_assume(__startrek_end[8] <= 8); __VERIFIER_assume(__startrek_max[8] < __startrek_min[9]); __VERIFIER_assume(__startrek_start[8] == __startrek_end[8]); __VERIFIER_assume(__startrek_min[8] == __startrek_start[8]); __VERIFIER_assume(__startrek_max[8] == __startrek_end[8]); __VERIFIER_assume(5 <= __startrek_start[7]); __VERIFIER_assume(__startrek_end[7] <= 7); __VERIFIER_assume(__startrek_max[7] < __startrek_min[8]); __VERIFIER_assume(__startrek_start[7] == __startrek_end[7]); __VERIFIER_assume(__startrek_min[7] == __startrek_start[7]); __VERIFIER_assume(__startrek_max[7] == __startrek_end[7]); __VERIFIER_assume(4 <= __startrek_start[6]); __VERIFIER_assume(__startrek_end[6] <= 6); __VERIFIER_assume(__startrek_max[6] < __startrek_min[7]); __VERIFIER_assume(__startrek_start[6] == __startrek_end[6]); __VERIFIER_assume(__startrek_min[6] == __startrek_start[6]); __VERIFIER_assume(__startrek_max[6] == __startrek_end[6]); __VERIFIER_assume(3 <= __startrek_start[5]); __VERIFIER_assume(__startrek_end[5] <= 5); __VERIFIER_assume(__startrek_max[5] < __startrek_min[6]); __VERIFIER_assume(__startrek_start[5] == __startrek_end[5]); __VERIFIER_assume(__startrek_min[5] == __startrek_start[5]); __VERIFIER_assume(__startrek_max[5] == __startrek_end[5]); __VERIFIER_assume(2 <= __startrek_start[4]); __VERIFIER_assume(__startrek_end[4] <= 4); __VERIFIER_assume(__startrek_max[4] < __startrek_min[5]); __VERIFIER_assume(__startrek_start[4] == __startrek_end[4]); __VERIFIER_assume(__startrek_min[4] == __startrek_start[4]); __VERIFIER_assume(__startrek_max[4] == __startrek_end[4]); __VERIFIER_assume(1 <= __startrek_start[3]); __VERIFIER_assume(__startrek_end[3] <= 3); __VERIFIER_assume(__startrek_max[3] < __startrek_min[4]); __VERIFIER_assume(__startrek_start[3] == __startrek_end[3]); __VERIFIER_assume(__startrek_min[3] == __startrek_start[3]); __VERIFIER_assume(__startrek_max[3] == __startrek_end[3]); __VERIFIER_assume(0 <= __startrek_start[2]); __VERIFIER_assume(__startrek_end[2] <= 2); __VERIFIER_assume(__startrek_max[2] < __startrek_min[3]); __VERIFIER_assume(__startrek_start[2] == __startrek_end[2]); __VERIFIER_assume(__startrek_min[2] == __startrek_start[2]); __VERIFIER_assume(__startrek_max[2] == __startrek_end[2]); __VERIFIER_assume(0 <= __startrek_start[1]); __VERIFIER_assume(__startrek_end[1] <= 13); __VERIFIER_assume(__startrek_max[1] < __startrek_min[14]); __VERIFIER_assume(__startrek_start[1] <= __startrek_end[1]); if (__startrek_start[1] < __startrek_min[2]) { __VERIFIER_assume(__startrek_min[1] == __startrek_start[1]); } else { __VERIFIER_assume(__startrek_min[1] == __startrek_min[2]); } if (__startrek_end[1] > __startrek_max[13]) { __VERIFIER_assume(__startrek_max[1] == __startrek_end[1]); } else { __VERIFIER_assume(__startrek_max[1] == __startrek_max[13]); } __VERIFIER_assume(0 <= __startrek_start[0]); __VERIFIER_assume(__startrek_end[0] <= 26); __VERIFIER_assume(__startrek_start[0] <= __startrek_end[0]); if (__startrek_start[0] < __startrek_min[1]) { __VERIFIER_assume(__startrek_min[0] == __startrek_start[0]); } else { __VERIFIER_assume(__startrek_min[0] == __startrek_min[1]); } if (__startrek_end[0] > __startrek_max[14]) { __VERIFIER_assume(__startrek_max[0] == __startrek_end[0]); } else { __VERIFIER_assume(__startrek_max[0] == __startrek_max[14]); } __VERIFIER_assume(__startrek_end[1] < __startrek_start[0]); __VERIFIER_assume(__startrek_end[2] < __startrek_start[1]); __VERIFIER_assume(__startrek_end[2] < __startrek_start[0]); __VERIFIER_assume(__startrek_end[3] <= __startrek_end[1]); if (__startrek_start[1] <= __startrek_end[3]) { if (__startrek_start[3] <= __startrek_end[1]) { { __VERIFIER_assume(__startrek_start[1] <= __startrek_start[3]); __VERIFIER_assume(__startrek_end[3] < __startrek_end[1]); } } } __VERIFIER_assume(__startrek_end[3] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[3]) { if (__startrek_start[3] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[3]); __VERIFIER_assume(__startrek_end[3] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[1] < __startrek_start[4]); __VERIFIER_assume(__startrek_end[4] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[4]) { if (__startrek_start[4] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[4]); __VERIFIER_assume(__startrek_end[4] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[1] < __startrek_start[5]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[5]); __VERIFIER_assume(__startrek_end[1] < __startrek_start[6]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[6]); __VERIFIER_assume(__startrek_end[1] < __startrek_start[7]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[7]); __VERIFIER_assume(__startrek_end[1] < __startrek_start[8]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[8]); __VERIFIER_assume(__startrek_end[1] < __startrek_start[9]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[9]); __VERIFIER_assume(__startrek_end[1] < __startrek_start[10]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[10]); __VERIFIER_assume(__startrek_end[1] < __startrek_start[11]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[11]); __VERIFIER_assume(__startrek_end[1] < __startrek_start[12]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[12]); __VERIFIER_assume(__startrek_end[1] < __startrek_start[13]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[13]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[14]); __VERIFIER_assume(__startrek_end[15] < __startrek_start[14]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[15]); __VERIFIER_assume(__startrek_end[16] <= __startrek_end[14]); if (__startrek_start[14] <= __startrek_end[16]) { if (__startrek_start[16] <= __startrek_end[14]) { { __VERIFIER_assume(__startrek_start[14] <= __startrek_start[16]); __VERIFIER_assume(__startrek_end[16] < __startrek_end[14]); } } } __VERIFIER_assume(__startrek_end[0] < __startrek_start[16]); __VERIFIER_assume(__startrek_end[14] < __startrek_start[17]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[17]); __VERIFIER_assume(__startrek_end[14] < __startrek_start[18]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[18]); __VERIFIER_assume(__startrek_end[14] < __startrek_start[19]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[19]); __VERIFIER_assume(__startrek_end[14] < __startrek_start[20]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[20]); __VERIFIER_assume(__startrek_end[14] < __startrek_start[21]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[21]); __VERIFIER_assume(__startrek_end[14] < __startrek_start[22]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[22]); __VERIFIER_assume(__startrek_end[14] < __startrek_start[23]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[23]); __VERIFIER_assume(__startrek_end[14] < __startrek_start[24]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[24]); __VERIFIER_assume(__startrek_end[14] < __startrek_start[25]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[25]); __VERIFIER_assume(__startrek_end[14] < __startrek_start[26]); __VERIFIER_assume(__startrek_end[0] < __startrek_start[26]); } } __inline void __startrek_init_globals(void) { { _i_observer_obstacle_flag_[1] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[1] = _i_observer_obstacle_flag_[1]; _i_observer_obstacle_flag_[2] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[2] = _i_observer_obstacle_flag_[2]; _i_observer_obstacle_flag_[3] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[3] = _i_observer_obstacle_flag_[3]; _i_observer_obstacle_flag_[4] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[4] = _i_observer_obstacle_flag_[4]; _i_observer_obstacle_flag_[5] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[5] = _i_observer_obstacle_flag_[5]; _i_observer_obstacle_flag_[6] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[6] = _i_observer_obstacle_flag_[6]; _i_observer_obstacle_flag_[7] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[7] = _i_observer_obstacle_flag_[7]; _i_observer_obstacle_flag_[8] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[8] = _i_observer_obstacle_flag_[8]; _i_observer_obstacle_flag_[9] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[9] = _i_observer_obstacle_flag_[9]; _i_observer_obstacle_flag_[10] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[10] = _i_observer_obstacle_flag_[10]; _i_observer_obstacle_flag_[11] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[11] = _i_observer_obstacle_flag_[11]; _i_observer_obstacle_flag_[12] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[12] = _i_observer_obstacle_flag_[12]; _i_observer_obstacle_flag_[13] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[13] = _i_observer_obstacle_flag_[13]; _i_observer_obstacle_flag_[14] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[14] = _i_observer_obstacle_flag_[14]; _i_observer_obstacle_flag_[15] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[15] = _i_observer_obstacle_flag_[15]; _i_observer_obstacle_flag_[16] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[16] = _i_observer_obstacle_flag_[16]; _i_observer_obstacle_flag_[17] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[17] = _i_observer_obstacle_flag_[17]; _i_observer_obstacle_flag_[18] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[18] = _i_observer_obstacle_flag_[18]; _i_observer_obstacle_flag_[19] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[19] = _i_observer_obstacle_flag_[19]; _i_observer_obstacle_flag_[20] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[20] = _i_observer_obstacle_flag_[20]; _i_observer_obstacle_flag_[21] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[21] = _i_observer_obstacle_flag_[21]; _i_observer_obstacle_flag_[22] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[22] = _i_observer_obstacle_flag_[22]; _i_observer_obstacle_flag_[23] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[23] = _i_observer_obstacle_flag_[23]; _i_observer_obstacle_flag_[24] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[24] = _i_observer_obstacle_flag_[24]; _i_observer_obstacle_flag_[25] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[25] = _i_observer_obstacle_flag_[25]; _i_observer_obstacle_flag_[26] = __VERIFIER_nondet_bool(); _observer_obstacle_flag_[26] = _i_observer_obstacle_flag_[26]; _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(); __VERIFIER_assume(__startrek_round > o2); __VERIFIER_assume(__startrek_round <= __startrek_job_end); if (__startrek_round != __startrek_job_end) { { switch (__startrek_job) { case 0: if (__startrek_start[26] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[26]); } if (__startrek_start[25] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[25]); } if (__startrek_start[24] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[24]); } if (__startrek_start[23] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[23]); } if (__startrek_start[22] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[22]); } if (__startrek_start[21] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[21]); } if (__startrek_start[20] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[20]); } if (__startrek_start[19] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[19]); } if (__startrek_start[18] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[18]); } if (__startrek_start[17] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[17]); } if (__startrek_start[16] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[16]); } if (__startrek_start[15] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[15]); } if (__startrek_start[14] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[14]); } if (__startrek_start[13] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[13]); } if (__startrek_start[12] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[12]); } if (__startrek_start[11] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[11]); } if (__startrek_start[10] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[10]); } if (__startrek_start[9] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[9]); } if (__startrek_start[8] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[8]); } if (__startrek_start[7] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[7]); } if (__startrek_start[6] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[6]); } if (__startrek_start[5] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[5]); } if (__startrek_start[4] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[4]); } if (__startrek_start[3] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[3]); } if (__startrek_start[2] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[2]); } if (__startrek_start[1] < __startrek_round) { __VERIFIER_assume(__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(); __VERIFIER_assume(__startrek_round > o2); __VERIFIER_assume(__startrek_round <= __startrek_job_end); if (__startrek_round != __startrek_job_end) { { switch (__startrek_job) { case 14: if (__startrek_start[26] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[26]); } if (__startrek_start[25] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[25]); } if (__startrek_start[24] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[24]); } if (__startrek_start[23] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[23]); } if (__startrek_start[22] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[22]); } if (__startrek_start[21] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[21]); } if (__startrek_start[20] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[20]); } if (__startrek_start[19] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[19]); } if (__startrek_start[18] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[18]); } if (__startrek_start[17] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[17]); } if (__startrek_start[16] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[16]); } if (__startrek_start[15] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[15]); } break; case 1: if (__startrek_start[13] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[13]); } if (__startrek_start[12] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[12]); } if (__startrek_start[11] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[11]); } if (__startrek_start[10] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[10]); } if (__startrek_start[9] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[9]); } if (__startrek_start[8] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[8]); } if (__startrek_start[7] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[7]); } if (__startrek_start[6] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[6]); } if (__startrek_start[5] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[5]); } if (__startrek_start[4] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[4]); } if (__startrek_start[3] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[3]); } if (__startrek_start[2] < __startrek_round) { __VERIFIER_assume(__startrek_round > __startrek_end[2]); } break; } } } return (1); } } __inline static _Bool __startrek_cs_t2(void) { { return (0); } } __inline static void __startrek_assert_i0(_Bool arg ) { { if (arg) { return; } switch (__startrek_task) { case 0: __startrek_Assert_t0_i0 = 0; break; case 1: __startrek_Assert_t1_i0 = 0; break; case 2: __startrek_Assert_t2_i0 = 0; break; } } } __inline void __startrek_user_init(void) { { } } __inline void __startrek_user_final(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_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 0: __VERIFIER_assume(_observer_obstacle_flag_[0] == _i_observer_obstacle_flag_[1]); __VERIFIER_assume(_obstacle_flag_[0] == _i_obstacle_flag_[1]); __VERIFIER_assume(_nxtway_gs_mode_[0] == _i_nxtway_gs_mode_[1]); break; case 1: __VERIFIER_assume(_observer_obstacle_flag_[1] == _i_observer_obstacle_flag_[2]); __VERIFIER_assume(_obstacle_flag_[1] == _i_obstacle_flag_[2]); __VERIFIER_assume(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); break; case 2: __VERIFIER_assume(_observer_obstacle_flag_[2] == _i_observer_obstacle_flag_[3]); __VERIFIER_assume(_obstacle_flag_[2] == _i_obstacle_flag_[3]); __VERIFIER_assume(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[1]; __startrek_task = 1; __startrek_job_end = __startrek_end[1]; __startrek_job = 1; __startrek_Assert_t1_i0 = 1; __startrek_entry_pt_OSEK_Task_ts2(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 0: __VERIFIER_assume(_observer_obstacle_flag_[0] == _i_observer_obstacle_flag_[1]); __VERIFIER_assume(_obstacle_flag_[0] == _i_obstacle_flag_[1]); __VERIFIER_assume(_nxtway_gs_mode_[0] == _i_nxtway_gs_mode_[1]); break; case 1: __VERIFIER_assume(_observer_obstacle_flag_[1] == _i_observer_obstacle_flag_[2]); __VERIFIER_assume(_obstacle_flag_[1] == _i_obstacle_flag_[2]); __VERIFIER_assume(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); break; case 2: __VERIFIER_assume(_observer_obstacle_flag_[2] == _i_observer_obstacle_flag_[3]); __VERIFIER_assume(_obstacle_flag_[2] == _i_obstacle_flag_[3]); __VERIFIER_assume(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); break; case 3: __VERIFIER_assume(_observer_obstacle_flag_[3] == _i_observer_obstacle_flag_[4]); __VERIFIER_assume(_obstacle_flag_[3] == _i_obstacle_flag_[4]); __VERIFIER_assume(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); break; case 4: __VERIFIER_assume(_observer_obstacle_flag_[4] == _i_observer_obstacle_flag_[5]); __VERIFIER_assume(_obstacle_flag_[4] == _i_obstacle_flag_[5]); __VERIFIER_assume(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); break; case 5: __VERIFIER_assume(_observer_obstacle_flag_[5] == _i_observer_obstacle_flag_[6]); __VERIFIER_assume(_obstacle_flag_[5] == _i_obstacle_flag_[6]); __VERIFIER_assume(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); break; case 6: __VERIFIER_assume(_observer_obstacle_flag_[6] == _i_observer_obstacle_flag_[7]); __VERIFIER_assume(_obstacle_flag_[6] == _i_obstacle_flag_[7]); __VERIFIER_assume(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); break; case 7: __VERIFIER_assume(_observer_obstacle_flag_[7] == _i_observer_obstacle_flag_[8]); __VERIFIER_assume(_obstacle_flag_[7] == _i_obstacle_flag_[8]); __VERIFIER_assume(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); break; case 8: __VERIFIER_assume(_observer_obstacle_flag_[8] == _i_observer_obstacle_flag_[9]); __VERIFIER_assume(_obstacle_flag_[8] == _i_obstacle_flag_[9]); __VERIFIER_assume(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); break; case 9: __VERIFIER_assume(_observer_obstacle_flag_[9] == _i_observer_obstacle_flag_[10]); __VERIFIER_assume(_obstacle_flag_[9] == _i_obstacle_flag_[10]); __VERIFIER_assume(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); break; case 10: __VERIFIER_assume(_observer_obstacle_flag_[10] == _i_observer_obstacle_flag_[11]); __VERIFIER_assume(_obstacle_flag_[10] == _i_obstacle_flag_[11]); __VERIFIER_assume(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); break; case 11: __VERIFIER_assume(_observer_obstacle_flag_[11] == _i_observer_obstacle_flag_[12]); __VERIFIER_assume(_obstacle_flag_[11] == _i_obstacle_flag_[12]); __VERIFIER_assume(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); break; case 12: __VERIFIER_assume(_observer_obstacle_flag_[12] == _i_observer_obstacle_flag_[13]); __VERIFIER_assume(_obstacle_flag_[12] == _i_obstacle_flag_[13]); __VERIFIER_assume(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); break; case 13: __VERIFIER_assume(_observer_obstacle_flag_[13] == _i_observer_obstacle_flag_[14]); __VERIFIER_assume(_obstacle_flag_[13] == _i_obstacle_flag_[14]); __VERIFIER_assume(_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_Assert_t0_i0 = 1; __startrek_entry_pt_OSEK_Task_Background(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 0: __VERIFIER_assume(_observer_obstacle_flag_[0] == _i_observer_obstacle_flag_[1]); __VERIFIER_assume(_obstacle_flag_[0] == _i_obstacle_flag_[1]); __VERIFIER_assume(_nxtway_gs_mode_[0] == _i_nxtway_gs_mode_[1]); break; case 1: __VERIFIER_assume(_observer_obstacle_flag_[1] == _i_observer_obstacle_flag_[2]); __VERIFIER_assume(_obstacle_flag_[1] == _i_obstacle_flag_[2]); __VERIFIER_assume(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); break; case 2: __VERIFIER_assume(_observer_obstacle_flag_[2] == _i_observer_obstacle_flag_[3]); __VERIFIER_assume(_obstacle_flag_[2] == _i_obstacle_flag_[3]); __VERIFIER_assume(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); break; case 3: __VERIFIER_assume(_observer_obstacle_flag_[3] == _i_observer_obstacle_flag_[4]); __VERIFIER_assume(_obstacle_flag_[3] == _i_obstacle_flag_[4]); __VERIFIER_assume(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); break; case 4: __VERIFIER_assume(_observer_obstacle_flag_[4] == _i_observer_obstacle_flag_[5]); __VERIFIER_assume(_obstacle_flag_[4] == _i_obstacle_flag_[5]); __VERIFIER_assume(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); break; case 5: __VERIFIER_assume(_observer_obstacle_flag_[5] == _i_observer_obstacle_flag_[6]); __VERIFIER_assume(_obstacle_flag_[5] == _i_obstacle_flag_[6]); __VERIFIER_assume(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); break; case 6: __VERIFIER_assume(_observer_obstacle_flag_[6] == _i_observer_obstacle_flag_[7]); __VERIFIER_assume(_obstacle_flag_[6] == _i_obstacle_flag_[7]); __VERIFIER_assume(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); break; case 7: __VERIFIER_assume(_observer_obstacle_flag_[7] == _i_observer_obstacle_flag_[8]); __VERIFIER_assume(_obstacle_flag_[7] == _i_obstacle_flag_[8]); __VERIFIER_assume(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); break; case 8: __VERIFIER_assume(_observer_obstacle_flag_[8] == _i_observer_obstacle_flag_[9]); __VERIFIER_assume(_obstacle_flag_[8] == _i_obstacle_flag_[9]); __VERIFIER_assume(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); break; case 9: __VERIFIER_assume(_observer_obstacle_flag_[9] == _i_observer_obstacle_flag_[10]); __VERIFIER_assume(_obstacle_flag_[9] == _i_obstacle_flag_[10]); __VERIFIER_assume(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); break; case 10: __VERIFIER_assume(_observer_obstacle_flag_[10] == _i_observer_obstacle_flag_[11]); __VERIFIER_assume(_obstacle_flag_[10] == _i_obstacle_flag_[11]); __VERIFIER_assume(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); break; case 11: __VERIFIER_assume(_observer_obstacle_flag_[11] == _i_observer_obstacle_flag_[12]); __VERIFIER_assume(_obstacle_flag_[11] == _i_obstacle_flag_[12]); __VERIFIER_assume(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); break; case 12: __VERIFIER_assume(_observer_obstacle_flag_[12] == _i_observer_obstacle_flag_[13]); __VERIFIER_assume(_obstacle_flag_[12] == _i_obstacle_flag_[13]); __VERIFIER_assume(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); break; case 13: __VERIFIER_assume(_observer_obstacle_flag_[13] == _i_observer_obstacle_flag_[14]); __VERIFIER_assume(_obstacle_flag_[13] == _i_obstacle_flag_[14]); __VERIFIER_assume(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); break; case 14: __VERIFIER_assume(_observer_obstacle_flag_[14] == _i_observer_obstacle_flag_[15]); __VERIFIER_assume(_obstacle_flag_[14] == _i_obstacle_flag_[15]); __VERIFIER_assume(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); break; case 15: __VERIFIER_assume(_observer_obstacle_flag_[15] == _i_observer_obstacle_flag_[16]); __VERIFIER_assume(_obstacle_flag_[15] == _i_obstacle_flag_[16]); __VERIFIER_assume(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); break; case 16: __VERIFIER_assume(_observer_obstacle_flag_[16] == _i_observer_obstacle_flag_[17]); __VERIFIER_assume(_obstacle_flag_[16] == _i_obstacle_flag_[17]); __VERIFIER_assume(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); break; case 17: __VERIFIER_assume(_observer_obstacle_flag_[17] == _i_observer_obstacle_flag_[18]); __VERIFIER_assume(_obstacle_flag_[17] == _i_obstacle_flag_[18]); __VERIFIER_assume(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); break; case 18: __VERIFIER_assume(_observer_obstacle_flag_[18] == _i_observer_obstacle_flag_[19]); __VERIFIER_assume(_obstacle_flag_[18] == _i_obstacle_flag_[19]); __VERIFIER_assume(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); break; case 19: __VERIFIER_assume(_observer_obstacle_flag_[19] == _i_observer_obstacle_flag_[20]); __VERIFIER_assume(_obstacle_flag_[19] == _i_obstacle_flag_[20]); __VERIFIER_assume(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); break; case 20: __VERIFIER_assume(_observer_obstacle_flag_[20] == _i_observer_obstacle_flag_[21]); __VERIFIER_assume(_obstacle_flag_[20] == _i_obstacle_flag_[21]); __VERIFIER_assume(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); break; case 21: __VERIFIER_assume(_observer_obstacle_flag_[21] == _i_observer_obstacle_flag_[22]); __VERIFIER_assume(_obstacle_flag_[21] == _i_obstacle_flag_[22]); __VERIFIER_assume(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); break; case 22: __VERIFIER_assume(_observer_obstacle_flag_[22] == _i_observer_obstacle_flag_[23]); __VERIFIER_assume(_obstacle_flag_[22] == _i_obstacle_flag_[23]); __VERIFIER_assume(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); break; case 23: __VERIFIER_assume(_observer_obstacle_flag_[23] == _i_observer_obstacle_flag_[24]); __VERIFIER_assume(_obstacle_flag_[23] == _i_obstacle_flag_[24]); __VERIFIER_assume(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); break; case 24: __VERIFIER_assume(_observer_obstacle_flag_[24] == _i_observer_obstacle_flag_[25]); __VERIFIER_assume(_obstacle_flag_[24] == _i_obstacle_flag_[25]); __VERIFIER_assume(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); break; case 25: __VERIFIER_assume(_observer_obstacle_flag_[25] == _i_observer_obstacle_flag_[26]); __VERIFIER_assume(_obstacle_flag_[25] == _i_obstacle_flag_[26]); __VERIFIER_assume(_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_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 1: __VERIFIER_assume(_observer_obstacle_flag_[1] == _i_observer_obstacle_flag_[2]); __VERIFIER_assume(_obstacle_flag_[1] == _i_obstacle_flag_[2]); __VERIFIER_assume(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); break; case 2: __VERIFIER_assume(_observer_obstacle_flag_[2] == _i_observer_obstacle_flag_[3]); __VERIFIER_assume(_obstacle_flag_[2] == _i_obstacle_flag_[3]); __VERIFIER_assume(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); break; case 3: __VERIFIER_assume(_observer_obstacle_flag_[3] == _i_observer_obstacle_flag_[4]); __VERIFIER_assume(_obstacle_flag_[3] == _i_obstacle_flag_[4]); __VERIFIER_assume(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); break; } assert(__startrek_Assert_t2_i0); assert(__startrek_Assert_t1_i0); __startrek_round = __startrek_start[4]; __startrek_task = 2; __startrek_job_end = __startrek_end[4]; __startrek_job = 4; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 2: __VERIFIER_assume(_observer_obstacle_flag_[2] == _i_observer_obstacle_flag_[3]); __VERIFIER_assume(_obstacle_flag_[2] == _i_obstacle_flag_[3]); __VERIFIER_assume(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); break; case 3: __VERIFIER_assume(_observer_obstacle_flag_[3] == _i_observer_obstacle_flag_[4]); __VERIFIER_assume(_obstacle_flag_[3] == _i_obstacle_flag_[4]); __VERIFIER_assume(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); break; case 4: __VERIFIER_assume(_observer_obstacle_flag_[4] == _i_observer_obstacle_flag_[5]); __VERIFIER_assume(_obstacle_flag_[4] == _i_obstacle_flag_[5]); __VERIFIER_assume(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); break; } assert(__startrek_Assert_t2_i0); assert(__startrek_Assert_t0_i0); __startrek_round = __startrek_start[5]; __startrek_task = 2; __startrek_job_end = __startrek_end[5]; __startrek_job = 5; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 3: __VERIFIER_assume(_observer_obstacle_flag_[3] == _i_observer_obstacle_flag_[4]); __VERIFIER_assume(_obstacle_flag_[3] == _i_obstacle_flag_[4]); __VERIFIER_assume(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); break; case 4: __VERIFIER_assume(_observer_obstacle_flag_[4] == _i_observer_obstacle_flag_[5]); __VERIFIER_assume(_obstacle_flag_[4] == _i_obstacle_flag_[5]); __VERIFIER_assume(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); break; case 5: __VERIFIER_assume(_observer_obstacle_flag_[5] == _i_observer_obstacle_flag_[6]); __VERIFIER_assume(_obstacle_flag_[5] == _i_obstacle_flag_[6]); __VERIFIER_assume(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[6]; __startrek_task = 2; __startrek_job_end = __startrek_end[6]; __startrek_job = 6; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 4: __VERIFIER_assume(_observer_obstacle_flag_[4] == _i_observer_obstacle_flag_[5]); __VERIFIER_assume(_obstacle_flag_[4] == _i_obstacle_flag_[5]); __VERIFIER_assume(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); break; case 5: __VERIFIER_assume(_observer_obstacle_flag_[5] == _i_observer_obstacle_flag_[6]); __VERIFIER_assume(_obstacle_flag_[5] == _i_obstacle_flag_[6]); __VERIFIER_assume(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); break; case 6: __VERIFIER_assume(_observer_obstacle_flag_[6] == _i_observer_obstacle_flag_[7]); __VERIFIER_assume(_obstacle_flag_[6] == _i_obstacle_flag_[7]); __VERIFIER_assume(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[7]; __startrek_task = 2; __startrek_job_end = __startrek_end[7]; __startrek_job = 7; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 5: __VERIFIER_assume(_observer_obstacle_flag_[5] == _i_observer_obstacle_flag_[6]); __VERIFIER_assume(_obstacle_flag_[5] == _i_obstacle_flag_[6]); __VERIFIER_assume(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); break; case 6: __VERIFIER_assume(_observer_obstacle_flag_[6] == _i_observer_obstacle_flag_[7]); __VERIFIER_assume(_obstacle_flag_[6] == _i_obstacle_flag_[7]); __VERIFIER_assume(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); break; case 7: __VERIFIER_assume(_observer_obstacle_flag_[7] == _i_observer_obstacle_flag_[8]); __VERIFIER_assume(_obstacle_flag_[7] == _i_obstacle_flag_[8]); __VERIFIER_assume(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[8]; __startrek_task = 2; __startrek_job_end = __startrek_end[8]; __startrek_job = 8; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 6: __VERIFIER_assume(_observer_obstacle_flag_[6] == _i_observer_obstacle_flag_[7]); __VERIFIER_assume(_obstacle_flag_[6] == _i_obstacle_flag_[7]); __VERIFIER_assume(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); break; case 7: __VERIFIER_assume(_observer_obstacle_flag_[7] == _i_observer_obstacle_flag_[8]); __VERIFIER_assume(_obstacle_flag_[7] == _i_obstacle_flag_[8]); __VERIFIER_assume(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); break; case 8: __VERIFIER_assume(_observer_obstacle_flag_[8] == _i_observer_obstacle_flag_[9]); __VERIFIER_assume(_obstacle_flag_[8] == _i_obstacle_flag_[9]); __VERIFIER_assume(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[9]; __startrek_task = 2; __startrek_job_end = __startrek_end[9]; __startrek_job = 9; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 7: __VERIFIER_assume(_observer_obstacle_flag_[7] == _i_observer_obstacle_flag_[8]); __VERIFIER_assume(_obstacle_flag_[7] == _i_obstacle_flag_[8]); __VERIFIER_assume(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); break; case 8: __VERIFIER_assume(_observer_obstacle_flag_[8] == _i_observer_obstacle_flag_[9]); __VERIFIER_assume(_obstacle_flag_[8] == _i_obstacle_flag_[9]); __VERIFIER_assume(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); break; case 9: __VERIFIER_assume(_observer_obstacle_flag_[9] == _i_observer_obstacle_flag_[10]); __VERIFIER_assume(_obstacle_flag_[9] == _i_obstacle_flag_[10]); __VERIFIER_assume(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[10]; __startrek_task = 2; __startrek_job_end = __startrek_end[10]; __startrek_job = 10; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 8: __VERIFIER_assume(_observer_obstacle_flag_[8] == _i_observer_obstacle_flag_[9]); __VERIFIER_assume(_obstacle_flag_[8] == _i_obstacle_flag_[9]); __VERIFIER_assume(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); break; case 9: __VERIFIER_assume(_observer_obstacle_flag_[9] == _i_observer_obstacle_flag_[10]); __VERIFIER_assume(_obstacle_flag_[9] == _i_obstacle_flag_[10]); __VERIFIER_assume(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); break; case 10: __VERIFIER_assume(_observer_obstacle_flag_[10] == _i_observer_obstacle_flag_[11]); __VERIFIER_assume(_obstacle_flag_[10] == _i_obstacle_flag_[11]); __VERIFIER_assume(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[11]; __startrek_task = 2; __startrek_job_end = __startrek_end[11]; __startrek_job = 11; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 9: __VERIFIER_assume(_observer_obstacle_flag_[9] == _i_observer_obstacle_flag_[10]); __VERIFIER_assume(_obstacle_flag_[9] == _i_obstacle_flag_[10]); __VERIFIER_assume(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); break; case 10: __VERIFIER_assume(_observer_obstacle_flag_[10] == _i_observer_obstacle_flag_[11]); __VERIFIER_assume(_obstacle_flag_[10] == _i_obstacle_flag_[11]); __VERIFIER_assume(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); break; case 11: __VERIFIER_assume(_observer_obstacle_flag_[11] == _i_observer_obstacle_flag_[12]); __VERIFIER_assume(_obstacle_flag_[11] == _i_obstacle_flag_[12]); __VERIFIER_assume(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[12]; __startrek_task = 2; __startrek_job_end = __startrek_end[12]; __startrek_job = 12; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 10: __VERIFIER_assume(_observer_obstacle_flag_[10] == _i_observer_obstacle_flag_[11]); __VERIFIER_assume(_obstacle_flag_[10] == _i_obstacle_flag_[11]); __VERIFIER_assume(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); break; case 11: __VERIFIER_assume(_observer_obstacle_flag_[11] == _i_observer_obstacle_flag_[12]); __VERIFIER_assume(_obstacle_flag_[11] == _i_obstacle_flag_[12]); __VERIFIER_assume(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); break; case 12: __VERIFIER_assume(_observer_obstacle_flag_[12] == _i_observer_obstacle_flag_[13]); __VERIFIER_assume(_obstacle_flag_[12] == _i_obstacle_flag_[13]); __VERIFIER_assume(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[13]; __startrek_task = 2; __startrek_job_end = __startrek_end[13]; __startrek_job = 13; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 11: __VERIFIER_assume(_observer_obstacle_flag_[11] == _i_observer_obstacle_flag_[12]); __VERIFIER_assume(_obstacle_flag_[11] == _i_obstacle_flag_[12]); __VERIFIER_assume(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); break; case 12: __VERIFIER_assume(_observer_obstacle_flag_[12] == _i_observer_obstacle_flag_[13]); __VERIFIER_assume(_obstacle_flag_[12] == _i_obstacle_flag_[13]); __VERIFIER_assume(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); break; case 13: __VERIFIER_assume(_observer_obstacle_flag_[13] == _i_observer_obstacle_flag_[14]); __VERIFIER_assume(_obstacle_flag_[13] == _i_obstacle_flag_[14]); __VERIFIER_assume(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[15]; __startrek_task = 2; __startrek_job_end = __startrek_end[15]; __startrek_job = 15; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 13: __VERIFIER_assume(_observer_obstacle_flag_[13] == _i_observer_obstacle_flag_[14]); __VERIFIER_assume(_obstacle_flag_[13] == _i_obstacle_flag_[14]); __VERIFIER_assume(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); break; case 14: __VERIFIER_assume(_observer_obstacle_flag_[14] == _i_observer_obstacle_flag_[15]); __VERIFIER_assume(_obstacle_flag_[14] == _i_obstacle_flag_[15]); __VERIFIER_assume(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); break; case 15: __VERIFIER_assume(_observer_obstacle_flag_[15] == _i_observer_obstacle_flag_[16]); __VERIFIER_assume(_obstacle_flag_[15] == _i_obstacle_flag_[16]); __VERIFIER_assume(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[14]; __startrek_task = 1; __startrek_job_end = __startrek_end[14]; __startrek_job = 14; __startrek_Assert_t1_i0 = 1; __startrek_entry_pt_OSEK_Task_ts2(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 13: __VERIFIER_assume(_observer_obstacle_flag_[13] == _i_observer_obstacle_flag_[14]); __VERIFIER_assume(_obstacle_flag_[13] == _i_obstacle_flag_[14]); __VERIFIER_assume(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); break; case 14: __VERIFIER_assume(_observer_obstacle_flag_[14] == _i_observer_obstacle_flag_[15]); __VERIFIER_assume(_obstacle_flag_[14] == _i_obstacle_flag_[15]); __VERIFIER_assume(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); break; case 15: __VERIFIER_assume(_observer_obstacle_flag_[15] == _i_observer_obstacle_flag_[16]); __VERIFIER_assume(_obstacle_flag_[15] == _i_obstacle_flag_[16]); __VERIFIER_assume(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); break; case 16: __VERIFIER_assume(_observer_obstacle_flag_[16] == _i_observer_obstacle_flag_[17]); __VERIFIER_assume(_obstacle_flag_[16] == _i_obstacle_flag_[17]); __VERIFIER_assume(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); break; case 17: __VERIFIER_assume(_observer_obstacle_flag_[17] == _i_observer_obstacle_flag_[18]); __VERIFIER_assume(_obstacle_flag_[17] == _i_obstacle_flag_[18]); __VERIFIER_assume(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); break; case 18: __VERIFIER_assume(_observer_obstacle_flag_[18] == _i_observer_obstacle_flag_[19]); __VERIFIER_assume(_obstacle_flag_[18] == _i_obstacle_flag_[19]); __VERIFIER_assume(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); break; case 19: __VERIFIER_assume(_observer_obstacle_flag_[19] == _i_observer_obstacle_flag_[20]); __VERIFIER_assume(_obstacle_flag_[19] == _i_obstacle_flag_[20]); __VERIFIER_assume(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); break; case 20: __VERIFIER_assume(_observer_obstacle_flag_[20] == _i_observer_obstacle_flag_[21]); __VERIFIER_assume(_obstacle_flag_[20] == _i_obstacle_flag_[21]); __VERIFIER_assume(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); break; case 21: __VERIFIER_assume(_observer_obstacle_flag_[21] == _i_observer_obstacle_flag_[22]); __VERIFIER_assume(_obstacle_flag_[21] == _i_obstacle_flag_[22]); __VERIFIER_assume(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); break; case 22: __VERIFIER_assume(_observer_obstacle_flag_[22] == _i_observer_obstacle_flag_[23]); __VERIFIER_assume(_obstacle_flag_[22] == _i_obstacle_flag_[23]); __VERIFIER_assume(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); break; case 23: __VERIFIER_assume(_observer_obstacle_flag_[23] == _i_observer_obstacle_flag_[24]); __VERIFIER_assume(_obstacle_flag_[23] == _i_obstacle_flag_[24]); __VERIFIER_assume(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); break; case 24: __VERIFIER_assume(_observer_obstacle_flag_[24] == _i_observer_obstacle_flag_[25]); __VERIFIER_assume(_obstacle_flag_[24] == _i_obstacle_flag_[25]); __VERIFIER_assume(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); break; case 25: __VERIFIER_assume(_observer_obstacle_flag_[25] == _i_observer_obstacle_flag_[26]); __VERIFIER_assume(_obstacle_flag_[25] == _i_obstacle_flag_[26]); __VERIFIER_assume(_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_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 14: __VERIFIER_assume(_observer_obstacle_flag_[14] == _i_observer_obstacle_flag_[15]); __VERIFIER_assume(_obstacle_flag_[14] == _i_obstacle_flag_[15]); __VERIFIER_assume(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); break; case 15: __VERIFIER_assume(_observer_obstacle_flag_[15] == _i_observer_obstacle_flag_[16]); __VERIFIER_assume(_obstacle_flag_[15] == _i_obstacle_flag_[16]); __VERIFIER_assume(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); break; case 16: __VERIFIER_assume(_observer_obstacle_flag_[16] == _i_observer_obstacle_flag_[17]); __VERIFIER_assume(_obstacle_flag_[16] == _i_obstacle_flag_[17]); __VERIFIER_assume(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); break; } assert(__startrek_Assert_t2_i0); assert(__startrek_Assert_t1_i0); __startrek_round = __startrek_start[17]; __startrek_task = 2; __startrek_job_end = __startrek_end[17]; __startrek_job = 17; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 15: __VERIFIER_assume(_observer_obstacle_flag_[15] == _i_observer_obstacle_flag_[16]); __VERIFIER_assume(_obstacle_flag_[15] == _i_obstacle_flag_[16]); __VERIFIER_assume(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); break; case 16: __VERIFIER_assume(_observer_obstacle_flag_[16] == _i_observer_obstacle_flag_[17]); __VERIFIER_assume(_obstacle_flag_[16] == _i_obstacle_flag_[17]); __VERIFIER_assume(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); break; case 17: __VERIFIER_assume(_observer_obstacle_flag_[17] == _i_observer_obstacle_flag_[18]); __VERIFIER_assume(_obstacle_flag_[17] == _i_obstacle_flag_[18]); __VERIFIER_assume(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[18]; __startrek_task = 2; __startrek_job_end = __startrek_end[18]; __startrek_job = 18; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 16: __VERIFIER_assume(_observer_obstacle_flag_[16] == _i_observer_obstacle_flag_[17]); __VERIFIER_assume(_obstacle_flag_[16] == _i_obstacle_flag_[17]); __VERIFIER_assume(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); break; case 17: __VERIFIER_assume(_observer_obstacle_flag_[17] == _i_observer_obstacle_flag_[18]); __VERIFIER_assume(_obstacle_flag_[17] == _i_obstacle_flag_[18]); __VERIFIER_assume(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); break; case 18: __VERIFIER_assume(_observer_obstacle_flag_[18] == _i_observer_obstacle_flag_[19]); __VERIFIER_assume(_obstacle_flag_[18] == _i_obstacle_flag_[19]); __VERIFIER_assume(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[19]; __startrek_task = 2; __startrek_job_end = __startrek_end[19]; __startrek_job = 19; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 17: __VERIFIER_assume(_observer_obstacle_flag_[17] == _i_observer_obstacle_flag_[18]); __VERIFIER_assume(_obstacle_flag_[17] == _i_obstacle_flag_[18]); __VERIFIER_assume(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); break; case 18: __VERIFIER_assume(_observer_obstacle_flag_[18] == _i_observer_obstacle_flag_[19]); __VERIFIER_assume(_obstacle_flag_[18] == _i_obstacle_flag_[19]); __VERIFIER_assume(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); break; case 19: __VERIFIER_assume(_observer_obstacle_flag_[19] == _i_observer_obstacle_flag_[20]); __VERIFIER_assume(_obstacle_flag_[19] == _i_obstacle_flag_[20]); __VERIFIER_assume(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[20]; __startrek_task = 2; __startrek_job_end = __startrek_end[20]; __startrek_job = 20; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 18: __VERIFIER_assume(_observer_obstacle_flag_[18] == _i_observer_obstacle_flag_[19]); __VERIFIER_assume(_obstacle_flag_[18] == _i_obstacle_flag_[19]); __VERIFIER_assume(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); break; case 19: __VERIFIER_assume(_observer_obstacle_flag_[19] == _i_observer_obstacle_flag_[20]); __VERIFIER_assume(_obstacle_flag_[19] == _i_obstacle_flag_[20]); __VERIFIER_assume(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); break; case 20: __VERIFIER_assume(_observer_obstacle_flag_[20] == _i_observer_obstacle_flag_[21]); __VERIFIER_assume(_obstacle_flag_[20] == _i_obstacle_flag_[21]); __VERIFIER_assume(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[21]; __startrek_task = 2; __startrek_job_end = __startrek_end[21]; __startrek_job = 21; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 19: __VERIFIER_assume(_observer_obstacle_flag_[19] == _i_observer_obstacle_flag_[20]); __VERIFIER_assume(_obstacle_flag_[19] == _i_obstacle_flag_[20]); __VERIFIER_assume(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); break; case 20: __VERIFIER_assume(_observer_obstacle_flag_[20] == _i_observer_obstacle_flag_[21]); __VERIFIER_assume(_obstacle_flag_[20] == _i_obstacle_flag_[21]); __VERIFIER_assume(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); break; case 21: __VERIFIER_assume(_observer_obstacle_flag_[21] == _i_observer_obstacle_flag_[22]); __VERIFIER_assume(_obstacle_flag_[21] == _i_obstacle_flag_[22]); __VERIFIER_assume(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[22]; __startrek_task = 2; __startrek_job_end = __startrek_end[22]; __startrek_job = 22; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 20: __VERIFIER_assume(_observer_obstacle_flag_[20] == _i_observer_obstacle_flag_[21]); __VERIFIER_assume(_obstacle_flag_[20] == _i_obstacle_flag_[21]); __VERIFIER_assume(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); break; case 21: __VERIFIER_assume(_observer_obstacle_flag_[21] == _i_observer_obstacle_flag_[22]); __VERIFIER_assume(_obstacle_flag_[21] == _i_obstacle_flag_[22]); __VERIFIER_assume(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); break; case 22: __VERIFIER_assume(_observer_obstacle_flag_[22] == _i_observer_obstacle_flag_[23]); __VERIFIER_assume(_obstacle_flag_[22] == _i_obstacle_flag_[23]); __VERIFIER_assume(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[23]; __startrek_task = 2; __startrek_job_end = __startrek_end[23]; __startrek_job = 23; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 21: __VERIFIER_assume(_observer_obstacle_flag_[21] == _i_observer_obstacle_flag_[22]); __VERIFIER_assume(_obstacle_flag_[21] == _i_obstacle_flag_[22]); __VERIFIER_assume(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); break; case 22: __VERIFIER_assume(_observer_obstacle_flag_[22] == _i_observer_obstacle_flag_[23]); __VERIFIER_assume(_obstacle_flag_[22] == _i_obstacle_flag_[23]); __VERIFIER_assume(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); break; case 23: __VERIFIER_assume(_observer_obstacle_flag_[23] == _i_observer_obstacle_flag_[24]); __VERIFIER_assume(_obstacle_flag_[23] == _i_obstacle_flag_[24]); __VERIFIER_assume(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[24]; __startrek_task = 2; __startrek_job_end = __startrek_end[24]; __startrek_job = 24; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 22: __VERIFIER_assume(_observer_obstacle_flag_[22] == _i_observer_obstacle_flag_[23]); __VERIFIER_assume(_obstacle_flag_[22] == _i_obstacle_flag_[23]); __VERIFIER_assume(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); break; case 23: __VERIFIER_assume(_observer_obstacle_flag_[23] == _i_observer_obstacle_flag_[24]); __VERIFIER_assume(_obstacle_flag_[23] == _i_obstacle_flag_[24]); __VERIFIER_assume(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); break; case 24: __VERIFIER_assume(_observer_obstacle_flag_[24] == _i_observer_obstacle_flag_[25]); __VERIFIER_assume(_obstacle_flag_[24] == _i_obstacle_flag_[25]); __VERIFIER_assume(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[25]; __startrek_task = 2; __startrek_job_end = __startrek_end[25]; __startrek_job = 25; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 23: __VERIFIER_assume(_observer_obstacle_flag_[23] == _i_observer_obstacle_flag_[24]); __VERIFIER_assume(_obstacle_flag_[23] == _i_obstacle_flag_[24]); __VERIFIER_assume(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); break; case 24: __VERIFIER_assume(_observer_obstacle_flag_[24] == _i_observer_obstacle_flag_[25]); __VERIFIER_assume(_obstacle_flag_[24] == _i_obstacle_flag_[25]); __VERIFIER_assume(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); break; case 25: __VERIFIER_assume(_observer_obstacle_flag_[25] == _i_observer_obstacle_flag_[26]); __VERIFIER_assume(_obstacle_flag_[25] == _i_obstacle_flag_[26]); __VERIFIER_assume(_nxtway_gs_mode_[25] == _i_nxtway_gs_mode_[26]); break; } assert(__startrek_Assert_t2_i0); __startrek_round = __startrek_start[26]; __startrek_task = 2; __startrek_job_end = __startrek_end[26]; __startrek_job = 26; __startrek_Assert_t2_i0 = 1; __startrek_entry_pt_OSEK_Task_ts1(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 24: __VERIFIER_assume(_observer_obstacle_flag_[24] == _i_observer_obstacle_flag_[25]); __VERIFIER_assume(_obstacle_flag_[24] == _i_obstacle_flag_[25]); __VERIFIER_assume(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); break; case 25: __VERIFIER_assume(_observer_obstacle_flag_[25] == _i_observer_obstacle_flag_[26]); __VERIFIER_assume(_obstacle_flag_[25] == _i_obstacle_flag_[26]); __VERIFIER_assume(_nxtway_gs_mode_[25] == _i_nxtway_gs_mode_[26]); break; } assert(__startrek_Assert_t2_i0); } } int main(void) { { __startrek_init_shared(); __startrek_user_init(); __startrek_hyper_period = 0; __startrek_hyperperiod(); _observer_obstacle_flag_[0] = _observer_obstacle_flag_[26]; _obstacle_flag_[0] = _obstacle_flag_[26]; _nxtway_gs_mode_[0] = _nxtway_gs_mode_[26]; __startrek_hyper_period = 1; __startrek_hyperperiod(); _observer_obstacle_flag_[0] = _observer_obstacle_flag_[26]; _obstacle_flag_[0] = _obstacle_flag_[26]; _nxtway_gs_mode_[0] = _nxtway_gs_mode_[26]; __startrek_hyper_period = 2; __startrek_hyperperiod(); _observer_obstacle_flag_[0] = _observer_obstacle_flag_[26]; _obstacle_flag_[0] = _obstacle_flag_[26]; _nxtway_gs_mode_[0] = _nxtway_gs_mode_[26]; __startrek_hyper_period = 3; __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 _Bool __startrek_read_observer_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 = _observer_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 static void __startrek_write_observer_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; } _observer_obstacle_flag_[__startrek_round] = arg; } } __inline void __startrek_init_shared(void) { { _observer_obstacle_flag_[0] = __startrek_hidden_observer_obstacle_flag; _obstacle_flag_[0] = __startrek_hidden_obstacle_flag; _nxtway_gs_mode_[0] = __startrek_hidden_nxtway_gs_mode; } }