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) ; char __VERIFIER_nondet_char(void) ; unsigned char __VERIFIER_nondet_uchar(void) ; _Bool __VERIFIER_nondet_bool(void) ; extern int __VERIFIER_nondet_int(); 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/aso.bug4.i","-S") extern void __startrek_cpu_lock(void) ; extern void __startrek_cpu_unlock(void) ; extern void __VERIFIER_assume(int ) ; void assert(_Bool arg) { if (!arg) { ERROR: __VERIFIER_error();} } extern void __startrek_get_pi_lock(char lock_id ) ; extern void __startrek_release_pi_lock(char lock_id ) ; int __startrek_pi_locks_held = 0; char __startrek_priority_locks[1] ; char __startrek_task_base_priority = 0; __inline static char __startrek_read___startrek_current_priority(void) ; __inline static void __startrek_write___startrek_current_priority(char arg ) ; char ___startrek_current_priority_[27] ; char _i___startrek_current_priority_[27] ; char __startrek_hidden___startrek_current_priority = 0; char __startrek_priority_locks[1] = { 1}; 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 char __startrek_read_cmd_forward(void) ; __inline static void __startrek_write_cmd_forward(char arg ) ; char _cmd_forward_[27] ; char _i_cmd_forward_[27] ; char __startrek_hidden_cmd_forward = 0; __inline static char __startrek_read_cmd_turn(void) ; __inline static void __startrek_write_cmd_turn(char arg ) ; char _cmd_turn_[27] ; char _i_cmd_turn_[27] ; char __startrek_hidden_cmd_turn = 0; __inline static _Bool __startrek_read_trans(void) ; __inline static void __startrek_write_trans(_Bool arg ) ; _Bool _trans_[27] ; _Bool _i_trans_[27] ; _Bool __startrek_hidden_trans = 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 ) ; 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 char task_cmd_forward ; static char task_cmd_turn ; void OSEK_Task_ts1(void) { char pwm_l ; char pwm_r ; _Bool lobstacle ; unsigned char tmp ; unsigned int tmp___0 ; unsigned int tmp___1 ; _Bool tmp___2 ; char tmp___3 ; char tmp___4 ; _Bool tmp___5 ; unsigned int tmp___6 ; char tmp___7 ; char tmp___8 ; unsigned int tmp___9 ; { lobstacle = 0; tmp = __startrek_read_nxtway_gs_mode(); switch (tmp) { case 0: gyro_offset = 0; avg_cnt = 0; 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: tmp___5 = __startrek_read_trans(); if (! tmp___5) { tmp___2 = __startrek_read_obstacle_flag(); lobstacle = tmp___2; tmp___3 = __startrek_read_cmd_turn(); task_cmd_turn = tmp___3; tmp___4 = __startrek_read_cmd_forward(); task_cmd_forward = tmp___4; } if (lobstacle) { __startrek_assert_i0((int )task_cmd_forward == -100 && (int )task_cmd_turn == 0); } tmp___6 = ecrobot_get_battery_voltage(); tmp___7 = nxt_motor_get_count(1); tmp___8 = nxt_motor_get_count(0); tmp___9 = ecrobot_get_gyro_sensor(3); balance_control((unsigned int )task_cmd_forward, (unsigned int )task_cmd_turn, tmp___9, gyro_offset, (unsigned int )tmp___8, (unsigned int )tmp___7, tmp___6, & pwm_l, & pwm_r); nxt_motor_set_speed(0, pwm_l, 1); nxt_motor_set_speed(1, pwm_r, 1); 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); __startrek_write_cmd_forward(-100); __startrek_write_cmd_turn(0); __startrek_write_trans(0); } } return; } } static unsigned char bt_receive_buf[2] ; void OSEK_Task_ts3(void) { int i ; _Bool wrote ; unsigned char tmp ; _Bool tmp___0 ; char tmp___1 ; char tmp___2 ; { wrote = 0; tmp = __startrek_read_nxtway_gs_mode(); switch (tmp) { case 0: i = 0; while (i < 2) { bt_receive_buf[i] = 0; i ++; } break; case 2: ecrobot_read_bt_packet(bt_receive_buf, 2); wrote = 0; __startrek_get_pi_lock(0); tmp___0 = __startrek_read_obstacle_flag(); if (! tmp___0) { __startrek_write_cmd_forward(- ((int )((char )bt_receive_buf[0]))); __startrek_write_cmd_turn((char )bt_receive_buf[1]); wrote = 1; } __startrek_release_pi_lock(0); if (wrote) { tmp___1 = __startrek_read_cmd_turn(); tmp___2 = __startrek_read_cmd_forward(); ecrobot_bt_data_logger(tmp___2, tmp___1); } break; default: break; } return; } } char __startrek_base_priority_OSEK_Task_ts3 = 0; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts3(void) ; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts3(void) { { OSEK_Task_ts3(); return ((_Bool)1); } } void cil_keeperOSEK_Task_ts3(void) { { __startrek_entry_pt_OSEK_Task_ts3(); return; } } int __startrek_period_OSEK_Task_ts3 = 96; int __startrek_wcet_OSEK_Task_ts3 = 48; int __startrek_arrival_min_OSEK_Task_ts3 = 0; int __startrek_arrival_max_OSEK_Task_ts3 = 0; char __startrek_base_priority_OSEK_Task_ts2 = 1; __inline static char __startrek_read___startrek_job_count_OSEK_Task_ts2(void) ; __inline static void __startrek_write___startrek_job_count_OSEK_Task_ts2(char arg ) ; char ___startrek_job_count_OSEK_Task_ts2_[27] ; char _i___startrek_job_count_OSEK_Task_ts2_[27] ; char __startrek_hidden___startrek_job_count_OSEK_Task_ts2 = 0; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts2(void) ; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts2(void) { char sp ; char tmp ; char tmp___0 ; { __startrek_lock = 1; tmp = __startrek_read___startrek_current_priority(); sp = tmp; __startrek_lock = 0; if ((int )__startrek_base_priority_OSEK_Task_ts2 <= (int )sp) { __VERIFIER_assume(0); return ((_Bool)0); } __startrek_lock = 1; __startrek_write___startrek_current_priority(__startrek_base_priority_OSEK_Task_ts2); __startrek_lock = 0; __startrek_pi_locks_held = 0; __startrek_task_base_priority = __startrek_base_priority_OSEK_Task_ts2; OSEK_Task_ts2(); __startrek_lock = 1; tmp___0 = __startrek_read___startrek_job_count_OSEK_Task_ts2(); __startrek_write___startrek_job_count_OSEK_Task_ts2(tmp___0 + 1); __startrek_write___startrek_current_priority(sp); __startrek_lock = 0; 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 = 24; 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 char __startrek_read___startrek_job_count_OSEK_Task_ts1(void) ; __inline static void __startrek_write___startrek_job_count_OSEK_Task_ts1(char arg ) ; char ___startrek_job_count_OSEK_Task_ts1_[27] ; char _i___startrek_job_count_OSEK_Task_ts1_[27] ; char __startrek_hidden___startrek_job_count_OSEK_Task_ts1 = 0; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts1(void) ; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts1(void) { char sp ; char tmp ; char tmp___0 ; { __startrek_lock = 1; tmp = __startrek_read___startrek_current_priority(); sp = tmp; __startrek_lock = 0; if ((int )__startrek_base_priority_OSEK_Task_ts1 <= (int )sp) { __VERIFIER_assume(0); return ((_Bool)0); } __startrek_lock = 1; __startrek_write___startrek_current_priority(__startrek_base_priority_OSEK_Task_ts1); __startrek_lock = 0; __startrek_pi_locks_held = 0; __startrek_task_base_priority = __startrek_base_priority_OSEK_Task_ts1; OSEK_Task_ts1(); __startrek_lock = 1; tmp___0 = __startrek_read___startrek_job_count_OSEK_Task_ts1(); __startrek_write___startrek_job_count_OSEK_Task_ts1(tmp___0 + 1); __startrek_write___startrek_current_priority(sp); __startrek_lock = 0; 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; 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[4] <= __startrek_end[1]); if (__startrek_start[1] <= __startrek_end[4]) { if (__startrek_start[4] <= __startrek_end[1]) { { __VERIFIER_assume(__startrek_start[1] <= __startrek_start[4]); __VERIFIER_assume(__startrek_end[4] < __startrek_end[1]); } } } __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[5] <= __startrek_end[1]); if (__startrek_start[1] <= __startrek_end[5]) { if (__startrek_start[5] <= __startrek_end[1]) { { __VERIFIER_assume(__startrek_start[1] <= __startrek_start[5]); __VERIFIER_assume(__startrek_end[5] < __startrek_end[1]); } } } __VERIFIER_assume(__startrek_end[5] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[5]) { if (__startrek_start[5] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[5]); __VERIFIER_assume(__startrek_end[5] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[6] <= __startrek_end[1]); if (__startrek_start[1] <= __startrek_end[6]) { if (__startrek_start[6] <= __startrek_end[1]) { { __VERIFIER_assume(__startrek_start[1] <= __startrek_start[6]); __VERIFIER_assume(__startrek_end[6] < __startrek_end[1]); } } } __VERIFIER_assume(__startrek_end[6] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[6]) { if (__startrek_start[6] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[6]); __VERIFIER_assume(__startrek_end[6] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[7] <= __startrek_end[1]); if (__startrek_start[1] <= __startrek_end[7]) { if (__startrek_start[7] <= __startrek_end[1]) { { __VERIFIER_assume(__startrek_start[1] <= __startrek_start[7]); __VERIFIER_assume(__startrek_end[7] < __startrek_end[1]); } } } __VERIFIER_assume(__startrek_end[7] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[7]) { if (__startrek_start[7] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[7]); __VERIFIER_assume(__startrek_end[7] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[8] <= __startrek_end[1]); if (__startrek_start[1] <= __startrek_end[8]) { if (__startrek_start[8] <= __startrek_end[1]) { { __VERIFIER_assume(__startrek_start[1] <= __startrek_start[8]); __VERIFIER_assume(__startrek_end[8] < __startrek_end[1]); } } } __VERIFIER_assume(__startrek_end[8] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[8]) { if (__startrek_start[8] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[8]); __VERIFIER_assume(__startrek_end[8] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[9] <= __startrek_end[1]); if (__startrek_start[1] <= __startrek_end[9]) { if (__startrek_start[9] <= __startrek_end[1]) { { __VERIFIER_assume(__startrek_start[1] <= __startrek_start[9]); __VERIFIER_assume(__startrek_end[9] < __startrek_end[1]); } } } __VERIFIER_assume(__startrek_end[9] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[9]) { if (__startrek_start[9] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[9]); __VERIFIER_assume(__startrek_end[9] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[1] < __startrek_start[10]); __VERIFIER_assume(__startrek_end[10] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[10]) { if (__startrek_start[10] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[10]); __VERIFIER_assume(__startrek_end[10] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[1] < __startrek_start[11]); __VERIFIER_assume(__startrek_end[11] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[11]) { if (__startrek_start[11] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[11]); __VERIFIER_assume(__startrek_end[11] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[1] < __startrek_start[12]); __VERIFIER_assume(__startrek_end[12] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[12]) { if (__startrek_start[12] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[12]); __VERIFIER_assume(__startrek_end[12] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[1] < __startrek_start[13]); __VERIFIER_assume(__startrek_end[13] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[13]) { if (__startrek_start[13] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[13]); __VERIFIER_assume(__startrek_end[13] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[14] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[14]) { if (__startrek_start[14] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[14]); __VERIFIER_assume(__startrek_end[14] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[15] < __startrek_start[14]); __VERIFIER_assume(__startrek_end[15] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[15]) { if (__startrek_start[15] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[15]); __VERIFIER_assume(__startrek_end[15] < __startrek_end[0]); } } } __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[16] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[16]) { if (__startrek_start[16] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[16]); __VERIFIER_assume(__startrek_end[16] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[17] <= __startrek_end[14]); if (__startrek_start[14] <= __startrek_end[17]) { if (__startrek_start[17] <= __startrek_end[14]) { { __VERIFIER_assume(__startrek_start[14] <= __startrek_start[17]); __VERIFIER_assume(__startrek_end[17] < __startrek_end[14]); } } } __VERIFIER_assume(__startrek_end[17] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[17]) { if (__startrek_start[17] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[17]); __VERIFIER_assume(__startrek_end[17] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[18] <= __startrek_end[14]); if (__startrek_start[14] <= __startrek_end[18]) { if (__startrek_start[18] <= __startrek_end[14]) { { __VERIFIER_assume(__startrek_start[14] <= __startrek_start[18]); __VERIFIER_assume(__startrek_end[18] < __startrek_end[14]); } } } __VERIFIER_assume(__startrek_end[18] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[18]) { if (__startrek_start[18] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[18]); __VERIFIER_assume(__startrek_end[18] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[19] <= __startrek_end[14]); if (__startrek_start[14] <= __startrek_end[19]) { if (__startrek_start[19] <= __startrek_end[14]) { { __VERIFIER_assume(__startrek_start[14] <= __startrek_start[19]); __VERIFIER_assume(__startrek_end[19] < __startrek_end[14]); } } } __VERIFIER_assume(__startrek_end[19] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[19]) { if (__startrek_start[19] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[19]); __VERIFIER_assume(__startrek_end[19] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[20] <= __startrek_end[14]); if (__startrek_start[14] <= __startrek_end[20]) { if (__startrek_start[20] <= __startrek_end[14]) { { __VERIFIER_assume(__startrek_start[14] <= __startrek_start[20]); __VERIFIER_assume(__startrek_end[20] < __startrek_end[14]); } } } __VERIFIER_assume(__startrek_end[20] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[20]) { if (__startrek_start[20] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[20]); __VERIFIER_assume(__startrek_end[20] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[21] <= __startrek_end[14]); if (__startrek_start[14] <= __startrek_end[21]) { if (__startrek_start[21] <= __startrek_end[14]) { { __VERIFIER_assume(__startrek_start[14] <= __startrek_start[21]); __VERIFIER_assume(__startrek_end[21] < __startrek_end[14]); } } } __VERIFIER_assume(__startrek_end[21] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[21]) { if (__startrek_start[21] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[21]); __VERIFIER_assume(__startrek_end[21] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[22] <= __startrek_end[14]); if (__startrek_start[14] <= __startrek_end[22]) { if (__startrek_start[22] <= __startrek_end[14]) { { __VERIFIER_assume(__startrek_start[14] <= __startrek_start[22]); __VERIFIER_assume(__startrek_end[22] < __startrek_end[14]); } } } __VERIFIER_assume(__startrek_end[22] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[22]) { if (__startrek_start[22] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[22]); __VERIFIER_assume(__startrek_end[22] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[14] < __startrek_start[23]); __VERIFIER_assume(__startrek_end[23] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[23]) { if (__startrek_start[23] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[23]); __VERIFIER_assume(__startrek_end[23] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[14] < __startrek_start[24]); __VERIFIER_assume(__startrek_end[24] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[24]) { if (__startrek_start[24] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[24]); __VERIFIER_assume(__startrek_end[24] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[14] < __startrek_start[25]); __VERIFIER_assume(__startrek_end[25] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[25]) { if (__startrek_start[25] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[25]); __VERIFIER_assume(__startrek_end[25] < __startrek_end[0]); } } } __VERIFIER_assume(__startrek_end[14] < __startrek_start[26]); __VERIFIER_assume(__startrek_end[26] <= __startrek_end[0]); if (__startrek_start[0] <= __startrek_end[26]) { if (__startrek_start[26] <= __startrek_end[0]) { { __VERIFIER_assume(__startrek_start[0] <= __startrek_start[26]); __VERIFIER_assume(__startrek_end[26] < __startrek_end[0]); } } } } } __inline void __startrek_init_globals(void) { { _i___startrek_job_count_OSEK_Task_ts1_[1] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[1] = _i___startrek_job_count_OSEK_Task_ts1_[1]; _i___startrek_job_count_OSEK_Task_ts1_[2] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[2] = _i___startrek_job_count_OSEK_Task_ts1_[2]; _i___startrek_job_count_OSEK_Task_ts1_[3] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[3] = _i___startrek_job_count_OSEK_Task_ts1_[3]; _i___startrek_job_count_OSEK_Task_ts1_[4] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[4] = _i___startrek_job_count_OSEK_Task_ts1_[4]; _i___startrek_job_count_OSEK_Task_ts1_[5] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[5] = _i___startrek_job_count_OSEK_Task_ts1_[5]; _i___startrek_job_count_OSEK_Task_ts1_[6] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[6] = _i___startrek_job_count_OSEK_Task_ts1_[6]; _i___startrek_job_count_OSEK_Task_ts1_[7] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[7] = _i___startrek_job_count_OSEK_Task_ts1_[7]; _i___startrek_job_count_OSEK_Task_ts1_[8] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[8] = _i___startrek_job_count_OSEK_Task_ts1_[8]; _i___startrek_job_count_OSEK_Task_ts1_[9] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[9] = _i___startrek_job_count_OSEK_Task_ts1_[9]; _i___startrek_job_count_OSEK_Task_ts1_[10] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[10] = _i___startrek_job_count_OSEK_Task_ts1_[10]; _i___startrek_job_count_OSEK_Task_ts1_[11] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[11] = _i___startrek_job_count_OSEK_Task_ts1_[11]; _i___startrek_job_count_OSEK_Task_ts1_[12] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[12] = _i___startrek_job_count_OSEK_Task_ts1_[12]; _i___startrek_job_count_OSEK_Task_ts1_[13] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[13] = _i___startrek_job_count_OSEK_Task_ts1_[13]; _i___startrek_job_count_OSEK_Task_ts1_[14] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[14] = _i___startrek_job_count_OSEK_Task_ts1_[14]; _i___startrek_job_count_OSEK_Task_ts1_[15] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[15] = _i___startrek_job_count_OSEK_Task_ts1_[15]; _i___startrek_job_count_OSEK_Task_ts1_[16] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[16] = _i___startrek_job_count_OSEK_Task_ts1_[16]; _i___startrek_job_count_OSEK_Task_ts1_[17] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[17] = _i___startrek_job_count_OSEK_Task_ts1_[17]; _i___startrek_job_count_OSEK_Task_ts1_[18] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[18] = _i___startrek_job_count_OSEK_Task_ts1_[18]; _i___startrek_job_count_OSEK_Task_ts1_[19] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[19] = _i___startrek_job_count_OSEK_Task_ts1_[19]; _i___startrek_job_count_OSEK_Task_ts1_[20] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[20] = _i___startrek_job_count_OSEK_Task_ts1_[20]; _i___startrek_job_count_OSEK_Task_ts1_[21] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[21] = _i___startrek_job_count_OSEK_Task_ts1_[21]; _i___startrek_job_count_OSEK_Task_ts1_[22] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[22] = _i___startrek_job_count_OSEK_Task_ts1_[22]; _i___startrek_job_count_OSEK_Task_ts1_[23] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[23] = _i___startrek_job_count_OSEK_Task_ts1_[23]; _i___startrek_job_count_OSEK_Task_ts1_[24] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[24] = _i___startrek_job_count_OSEK_Task_ts1_[24]; _i___startrek_job_count_OSEK_Task_ts1_[25] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[25] = _i___startrek_job_count_OSEK_Task_ts1_[25]; _i___startrek_job_count_OSEK_Task_ts1_[26] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts1_[26] = _i___startrek_job_count_OSEK_Task_ts1_[26]; _i___startrek_job_count_OSEK_Task_ts2_[1] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[1] = _i___startrek_job_count_OSEK_Task_ts2_[1]; _i___startrek_job_count_OSEK_Task_ts2_[2] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[2] = _i___startrek_job_count_OSEK_Task_ts2_[2]; _i___startrek_job_count_OSEK_Task_ts2_[3] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[3] = _i___startrek_job_count_OSEK_Task_ts2_[3]; _i___startrek_job_count_OSEK_Task_ts2_[4] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[4] = _i___startrek_job_count_OSEK_Task_ts2_[4]; _i___startrek_job_count_OSEK_Task_ts2_[5] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[5] = _i___startrek_job_count_OSEK_Task_ts2_[5]; _i___startrek_job_count_OSEK_Task_ts2_[6] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[6] = _i___startrek_job_count_OSEK_Task_ts2_[6]; _i___startrek_job_count_OSEK_Task_ts2_[7] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[7] = _i___startrek_job_count_OSEK_Task_ts2_[7]; _i___startrek_job_count_OSEK_Task_ts2_[8] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[8] = _i___startrek_job_count_OSEK_Task_ts2_[8]; _i___startrek_job_count_OSEK_Task_ts2_[9] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[9] = _i___startrek_job_count_OSEK_Task_ts2_[9]; _i___startrek_job_count_OSEK_Task_ts2_[10] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[10] = _i___startrek_job_count_OSEK_Task_ts2_[10]; _i___startrek_job_count_OSEK_Task_ts2_[11] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[11] = _i___startrek_job_count_OSEK_Task_ts2_[11]; _i___startrek_job_count_OSEK_Task_ts2_[12] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[12] = _i___startrek_job_count_OSEK_Task_ts2_[12]; _i___startrek_job_count_OSEK_Task_ts2_[13] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[13] = _i___startrek_job_count_OSEK_Task_ts2_[13]; _i___startrek_job_count_OSEK_Task_ts2_[14] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[14] = _i___startrek_job_count_OSEK_Task_ts2_[14]; _i___startrek_job_count_OSEK_Task_ts2_[15] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[15] = _i___startrek_job_count_OSEK_Task_ts2_[15]; _i___startrek_job_count_OSEK_Task_ts2_[16] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[16] = _i___startrek_job_count_OSEK_Task_ts2_[16]; _i___startrek_job_count_OSEK_Task_ts2_[17] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[17] = _i___startrek_job_count_OSEK_Task_ts2_[17]; _i___startrek_job_count_OSEK_Task_ts2_[18] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[18] = _i___startrek_job_count_OSEK_Task_ts2_[18]; _i___startrek_job_count_OSEK_Task_ts2_[19] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[19] = _i___startrek_job_count_OSEK_Task_ts2_[19]; _i___startrek_job_count_OSEK_Task_ts2_[20] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[20] = _i___startrek_job_count_OSEK_Task_ts2_[20]; _i___startrek_job_count_OSEK_Task_ts2_[21] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[21] = _i___startrek_job_count_OSEK_Task_ts2_[21]; _i___startrek_job_count_OSEK_Task_ts2_[22] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[22] = _i___startrek_job_count_OSEK_Task_ts2_[22]; _i___startrek_job_count_OSEK_Task_ts2_[23] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[23] = _i___startrek_job_count_OSEK_Task_ts2_[23]; _i___startrek_job_count_OSEK_Task_ts2_[24] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[24] = _i___startrek_job_count_OSEK_Task_ts2_[24]; _i___startrek_job_count_OSEK_Task_ts2_[25] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[25] = _i___startrek_job_count_OSEK_Task_ts2_[25]; _i___startrek_job_count_OSEK_Task_ts2_[26] = __VERIFIER_nondet_char(); ___startrek_job_count_OSEK_Task_ts2_[26] = _i___startrek_job_count_OSEK_Task_ts2_[26]; _i_trans_[1] = __VERIFIER_nondet_bool(); _trans_[1] = _i_trans_[1]; _i_trans_[2] = __VERIFIER_nondet_bool(); _trans_[2] = _i_trans_[2]; _i_trans_[3] = __VERIFIER_nondet_bool(); _trans_[3] = _i_trans_[3]; _i_trans_[4] = __VERIFIER_nondet_bool(); _trans_[4] = _i_trans_[4]; _i_trans_[5] = __VERIFIER_nondet_bool(); _trans_[5] = _i_trans_[5]; _i_trans_[6] = __VERIFIER_nondet_bool(); _trans_[6] = _i_trans_[6]; _i_trans_[7] = __VERIFIER_nondet_bool(); _trans_[7] = _i_trans_[7]; _i_trans_[8] = __VERIFIER_nondet_bool(); _trans_[8] = _i_trans_[8]; _i_trans_[9] = __VERIFIER_nondet_bool(); _trans_[9] = _i_trans_[9]; _i_trans_[10] = __VERIFIER_nondet_bool(); _trans_[10] = _i_trans_[10]; _i_trans_[11] = __VERIFIER_nondet_bool(); _trans_[11] = _i_trans_[11]; _i_trans_[12] = __VERIFIER_nondet_bool(); _trans_[12] = _i_trans_[12]; _i_trans_[13] = __VERIFIER_nondet_bool(); _trans_[13] = _i_trans_[13]; _i_trans_[14] = __VERIFIER_nondet_bool(); _trans_[14] = _i_trans_[14]; _i_trans_[15] = __VERIFIER_nondet_bool(); _trans_[15] = _i_trans_[15]; _i_trans_[16] = __VERIFIER_nondet_bool(); _trans_[16] = _i_trans_[16]; _i_trans_[17] = __VERIFIER_nondet_bool(); _trans_[17] = _i_trans_[17]; _i_trans_[18] = __VERIFIER_nondet_bool(); _trans_[18] = _i_trans_[18]; _i_trans_[19] = __VERIFIER_nondet_bool(); _trans_[19] = _i_trans_[19]; _i_trans_[20] = __VERIFIER_nondet_bool(); _trans_[20] = _i_trans_[20]; _i_trans_[21] = __VERIFIER_nondet_bool(); _trans_[21] = _i_trans_[21]; _i_trans_[22] = __VERIFIER_nondet_bool(); _trans_[22] = _i_trans_[22]; _i_trans_[23] = __VERIFIER_nondet_bool(); _trans_[23] = _i_trans_[23]; _i_trans_[24] = __VERIFIER_nondet_bool(); _trans_[24] = _i_trans_[24]; _i_trans_[25] = __VERIFIER_nondet_bool(); _trans_[25] = _i_trans_[25]; _i_trans_[26] = __VERIFIER_nondet_bool(); _trans_[26] = _i_trans_[26]; _i_cmd_turn_[1] = __VERIFIER_nondet_char(); _cmd_turn_[1] = _i_cmd_turn_[1]; _i_cmd_turn_[2] = __VERIFIER_nondet_char(); _cmd_turn_[2] = _i_cmd_turn_[2]; _i_cmd_turn_[3] = __VERIFIER_nondet_char(); _cmd_turn_[3] = _i_cmd_turn_[3]; _i_cmd_turn_[4] = __VERIFIER_nondet_char(); _cmd_turn_[4] = _i_cmd_turn_[4]; _i_cmd_turn_[5] = __VERIFIER_nondet_char(); _cmd_turn_[5] = _i_cmd_turn_[5]; _i_cmd_turn_[6] = __VERIFIER_nondet_char(); _cmd_turn_[6] = _i_cmd_turn_[6]; _i_cmd_turn_[7] = __VERIFIER_nondet_char(); _cmd_turn_[7] = _i_cmd_turn_[7]; _i_cmd_turn_[8] = __VERIFIER_nondet_char(); _cmd_turn_[8] = _i_cmd_turn_[8]; _i_cmd_turn_[9] = __VERIFIER_nondet_char(); _cmd_turn_[9] = _i_cmd_turn_[9]; _i_cmd_turn_[10] = __VERIFIER_nondet_char(); _cmd_turn_[10] = _i_cmd_turn_[10]; _i_cmd_turn_[11] = __VERIFIER_nondet_char(); _cmd_turn_[11] = _i_cmd_turn_[11]; _i_cmd_turn_[12] = __VERIFIER_nondet_char(); _cmd_turn_[12] = _i_cmd_turn_[12]; _i_cmd_turn_[13] = __VERIFIER_nondet_char(); _cmd_turn_[13] = _i_cmd_turn_[13]; _i_cmd_turn_[14] = __VERIFIER_nondet_char(); _cmd_turn_[14] = _i_cmd_turn_[14]; _i_cmd_turn_[15] = __VERIFIER_nondet_char(); _cmd_turn_[15] = _i_cmd_turn_[15]; _i_cmd_turn_[16] = __VERIFIER_nondet_char(); _cmd_turn_[16] = _i_cmd_turn_[16]; _i_cmd_turn_[17] = __VERIFIER_nondet_char(); _cmd_turn_[17] = _i_cmd_turn_[17]; _i_cmd_turn_[18] = __VERIFIER_nondet_char(); _cmd_turn_[18] = _i_cmd_turn_[18]; _i_cmd_turn_[19] = __VERIFIER_nondet_char(); _cmd_turn_[19] = _i_cmd_turn_[19]; _i_cmd_turn_[20] = __VERIFIER_nondet_char(); _cmd_turn_[20] = _i_cmd_turn_[20]; _i_cmd_turn_[21] = __VERIFIER_nondet_char(); _cmd_turn_[21] = _i_cmd_turn_[21]; _i_cmd_turn_[22] = __VERIFIER_nondet_char(); _cmd_turn_[22] = _i_cmd_turn_[22]; _i_cmd_turn_[23] = __VERIFIER_nondet_char(); _cmd_turn_[23] = _i_cmd_turn_[23]; _i_cmd_turn_[24] = __VERIFIER_nondet_char(); _cmd_turn_[24] = _i_cmd_turn_[24]; _i_cmd_turn_[25] = __VERIFIER_nondet_char(); _cmd_turn_[25] = _i_cmd_turn_[25]; _i_cmd_turn_[26] = __VERIFIER_nondet_char(); _cmd_turn_[26] = _i_cmd_turn_[26]; _i_cmd_forward_[1] = __VERIFIER_nondet_char(); _cmd_forward_[1] = _i_cmd_forward_[1]; _i_cmd_forward_[2] = __VERIFIER_nondet_char(); _cmd_forward_[2] = _i_cmd_forward_[2]; _i_cmd_forward_[3] = __VERIFIER_nondet_char(); _cmd_forward_[3] = _i_cmd_forward_[3]; _i_cmd_forward_[4] = __VERIFIER_nondet_char(); _cmd_forward_[4] = _i_cmd_forward_[4]; _i_cmd_forward_[5] = __VERIFIER_nondet_char(); _cmd_forward_[5] = _i_cmd_forward_[5]; _i_cmd_forward_[6] = __VERIFIER_nondet_char(); _cmd_forward_[6] = _i_cmd_forward_[6]; _i_cmd_forward_[7] = __VERIFIER_nondet_char(); _cmd_forward_[7] = _i_cmd_forward_[7]; _i_cmd_forward_[8] = __VERIFIER_nondet_char(); _cmd_forward_[8] = _i_cmd_forward_[8]; _i_cmd_forward_[9] = __VERIFIER_nondet_char(); _cmd_forward_[9] = _i_cmd_forward_[9]; _i_cmd_forward_[10] = __VERIFIER_nondet_char(); _cmd_forward_[10] = _i_cmd_forward_[10]; _i_cmd_forward_[11] = __VERIFIER_nondet_char(); _cmd_forward_[11] = _i_cmd_forward_[11]; _i_cmd_forward_[12] = __VERIFIER_nondet_char(); _cmd_forward_[12] = _i_cmd_forward_[12]; _i_cmd_forward_[13] = __VERIFIER_nondet_char(); _cmd_forward_[13] = _i_cmd_forward_[13]; _i_cmd_forward_[14] = __VERIFIER_nondet_char(); _cmd_forward_[14] = _i_cmd_forward_[14]; _i_cmd_forward_[15] = __VERIFIER_nondet_char(); _cmd_forward_[15] = _i_cmd_forward_[15]; _i_cmd_forward_[16] = __VERIFIER_nondet_char(); _cmd_forward_[16] = _i_cmd_forward_[16]; _i_cmd_forward_[17] = __VERIFIER_nondet_char(); _cmd_forward_[17] = _i_cmd_forward_[17]; _i_cmd_forward_[18] = __VERIFIER_nondet_char(); _cmd_forward_[18] = _i_cmd_forward_[18]; _i_cmd_forward_[19] = __VERIFIER_nondet_char(); _cmd_forward_[19] = _i_cmd_forward_[19]; _i_cmd_forward_[20] = __VERIFIER_nondet_char(); _cmd_forward_[20] = _i_cmd_forward_[20]; _i_cmd_forward_[21] = __VERIFIER_nondet_char(); _cmd_forward_[21] = _i_cmd_forward_[21]; _i_cmd_forward_[22] = __VERIFIER_nondet_char(); _cmd_forward_[22] = _i_cmd_forward_[22]; _i_cmd_forward_[23] = __VERIFIER_nondet_char(); _cmd_forward_[23] = _i_cmd_forward_[23]; _i_cmd_forward_[24] = __VERIFIER_nondet_char(); _cmd_forward_[24] = _i_cmd_forward_[24]; _i_cmd_forward_[25] = __VERIFIER_nondet_char(); _cmd_forward_[25] = _i_cmd_forward_[25]; _i_cmd_forward_[26] = __VERIFIER_nondet_char(); _cmd_forward_[26] = _i_cmd_forward_[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]; _i___startrek_current_priority_[1] = __VERIFIER_nondet_char(); ___startrek_current_priority_[1] = _i___startrek_current_priority_[1]; _i___startrek_current_priority_[2] = __VERIFIER_nondet_char(); ___startrek_current_priority_[2] = _i___startrek_current_priority_[2]; _i___startrek_current_priority_[3] = __VERIFIER_nondet_char(); ___startrek_current_priority_[3] = _i___startrek_current_priority_[3]; _i___startrek_current_priority_[4] = __VERIFIER_nondet_char(); ___startrek_current_priority_[4] = _i___startrek_current_priority_[4]; _i___startrek_current_priority_[5] = __VERIFIER_nondet_char(); ___startrek_current_priority_[5] = _i___startrek_current_priority_[5]; _i___startrek_current_priority_[6] = __VERIFIER_nondet_char(); ___startrek_current_priority_[6] = _i___startrek_current_priority_[6]; _i___startrek_current_priority_[7] = __VERIFIER_nondet_char(); ___startrek_current_priority_[7] = _i___startrek_current_priority_[7]; _i___startrek_current_priority_[8] = __VERIFIER_nondet_char(); ___startrek_current_priority_[8] = _i___startrek_current_priority_[8]; _i___startrek_current_priority_[9] = __VERIFIER_nondet_char(); ___startrek_current_priority_[9] = _i___startrek_current_priority_[9]; _i___startrek_current_priority_[10] = __VERIFIER_nondet_char(); ___startrek_current_priority_[10] = _i___startrek_current_priority_[10]; _i___startrek_current_priority_[11] = __VERIFIER_nondet_char(); ___startrek_current_priority_[11] = _i___startrek_current_priority_[11]; _i___startrek_current_priority_[12] = __VERIFIER_nondet_char(); ___startrek_current_priority_[12] = _i___startrek_current_priority_[12]; _i___startrek_current_priority_[13] = __VERIFIER_nondet_char(); ___startrek_current_priority_[13] = _i___startrek_current_priority_[13]; _i___startrek_current_priority_[14] = __VERIFIER_nondet_char(); ___startrek_current_priority_[14] = _i___startrek_current_priority_[14]; _i___startrek_current_priority_[15] = __VERIFIER_nondet_char(); ___startrek_current_priority_[15] = _i___startrek_current_priority_[15]; _i___startrek_current_priority_[16] = __VERIFIER_nondet_char(); ___startrek_current_priority_[16] = _i___startrek_current_priority_[16]; _i___startrek_current_priority_[17] = __VERIFIER_nondet_char(); ___startrek_current_priority_[17] = _i___startrek_current_priority_[17]; _i___startrek_current_priority_[18] = __VERIFIER_nondet_char(); ___startrek_current_priority_[18] = _i___startrek_current_priority_[18]; _i___startrek_current_priority_[19] = __VERIFIER_nondet_char(); ___startrek_current_priority_[19] = _i___startrek_current_priority_[19]; _i___startrek_current_priority_[20] = __VERIFIER_nondet_char(); ___startrek_current_priority_[20] = _i___startrek_current_priority_[20]; _i___startrek_current_priority_[21] = __VERIFIER_nondet_char(); ___startrek_current_priority_[21] = _i___startrek_current_priority_[21]; _i___startrek_current_priority_[22] = __VERIFIER_nondet_char(); ___startrek_current_priority_[22] = _i___startrek_current_priority_[22]; _i___startrek_current_priority_[23] = __VERIFIER_nondet_char(); ___startrek_current_priority_[23] = _i___startrek_current_priority_[23]; _i___startrek_current_priority_[24] = __VERIFIER_nondet_char(); ___startrek_current_priority_[24] = _i___startrek_current_priority_[24]; _i___startrek_current_priority_[25] = __VERIFIER_nondet_char(); ___startrek_current_priority_[25] = _i___startrek_current_priority_[25]; _i___startrek_current_priority_[26] = __VERIFIER_nondet_char(); ___startrek_current_priority_[26] = _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[0] == _i___startrek_job_count_OSEK_Task_ts1_[1]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[0] == _i___startrek_job_count_OSEK_Task_ts2_[1]); __VERIFIER_assume(_trans_[0] == _i_trans_[1]); __VERIFIER_assume(_cmd_turn_[0] == _i_cmd_turn_[1]); __VERIFIER_assume(_cmd_forward_[0] == _i_cmd_forward_[1]); __VERIFIER_assume(_obstacle_flag_[0] == _i_obstacle_flag_[1]); __VERIFIER_assume(_nxtway_gs_mode_[0] == _i_nxtway_gs_mode_[1]); __VERIFIER_assume(___startrek_current_priority_[0] == _i___startrek_current_priority_[1]); break; case 1: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[1] == _i___startrek_job_count_OSEK_Task_ts1_[2]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[1] == _i___startrek_job_count_OSEK_Task_ts2_[2]); __VERIFIER_assume(_trans_[1] == _i_trans_[2]); __VERIFIER_assume(_cmd_turn_[1] == _i_cmd_turn_[2]); __VERIFIER_assume(_cmd_forward_[1] == _i_cmd_forward_[2]); __VERIFIER_assume(_obstacle_flag_[1] == _i_obstacle_flag_[2]); __VERIFIER_assume(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); __VERIFIER_assume(___startrek_current_priority_[1] == _i___startrek_current_priority_[2]); break; case 2: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[2] == _i___startrek_job_count_OSEK_Task_ts1_[3]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[2] == _i___startrek_job_count_OSEK_Task_ts2_[3]); __VERIFIER_assume(_trans_[2] == _i_trans_[3]); __VERIFIER_assume(_cmd_turn_[2] == _i_cmd_turn_[3]); __VERIFIER_assume(_cmd_forward_[2] == _i_cmd_forward_[3]); __VERIFIER_assume(_obstacle_flag_[2] == _i_obstacle_flag_[3]); __VERIFIER_assume(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); __VERIFIER_assume(___startrek_current_priority_[2] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[0] == _i___startrek_job_count_OSEK_Task_ts1_[1]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[0] == _i___startrek_job_count_OSEK_Task_ts2_[1]); __VERIFIER_assume(_trans_[0] == _i_trans_[1]); __VERIFIER_assume(_cmd_turn_[0] == _i_cmd_turn_[1]); __VERIFIER_assume(_cmd_forward_[0] == _i_cmd_forward_[1]); __VERIFIER_assume(_obstacle_flag_[0] == _i_obstacle_flag_[1]); __VERIFIER_assume(_nxtway_gs_mode_[0] == _i_nxtway_gs_mode_[1]); __VERIFIER_assume(___startrek_current_priority_[0] == _i___startrek_current_priority_[1]); break; case 1: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[1] == _i___startrek_job_count_OSEK_Task_ts1_[2]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[1] == _i___startrek_job_count_OSEK_Task_ts2_[2]); __VERIFIER_assume(_trans_[1] == _i_trans_[2]); __VERIFIER_assume(_cmd_turn_[1] == _i_cmd_turn_[2]); __VERIFIER_assume(_cmd_forward_[1] == _i_cmd_forward_[2]); __VERIFIER_assume(_obstacle_flag_[1] == _i_obstacle_flag_[2]); __VERIFIER_assume(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); __VERIFIER_assume(___startrek_current_priority_[1] == _i___startrek_current_priority_[2]); break; case 2: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[2] == _i___startrek_job_count_OSEK_Task_ts1_[3]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[2] == _i___startrek_job_count_OSEK_Task_ts2_[3]); __VERIFIER_assume(_trans_[2] == _i_trans_[3]); __VERIFIER_assume(_cmd_turn_[2] == _i_cmd_turn_[3]); __VERIFIER_assume(_cmd_forward_[2] == _i_cmd_forward_[3]); __VERIFIER_assume(_obstacle_flag_[2] == _i_obstacle_flag_[3]); __VERIFIER_assume(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); __VERIFIER_assume(___startrek_current_priority_[2] == _i___startrek_current_priority_[3]); break; case 3: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[3] == _i___startrek_job_count_OSEK_Task_ts1_[4]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[3] == _i___startrek_job_count_OSEK_Task_ts2_[4]); __VERIFIER_assume(_trans_[3] == _i_trans_[4]); __VERIFIER_assume(_cmd_turn_[3] == _i_cmd_turn_[4]); __VERIFIER_assume(_cmd_forward_[3] == _i_cmd_forward_[4]); __VERIFIER_assume(_obstacle_flag_[3] == _i_obstacle_flag_[4]); __VERIFIER_assume(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); __VERIFIER_assume(___startrek_current_priority_[3] == _i___startrek_current_priority_[4]); break; case 4: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[4] == _i___startrek_job_count_OSEK_Task_ts1_[5]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[4] == _i___startrek_job_count_OSEK_Task_ts2_[5]); __VERIFIER_assume(_trans_[4] == _i_trans_[5]); __VERIFIER_assume(_cmd_turn_[4] == _i_cmd_turn_[5]); __VERIFIER_assume(_cmd_forward_[4] == _i_cmd_forward_[5]); __VERIFIER_assume(_obstacle_flag_[4] == _i_obstacle_flag_[5]); __VERIFIER_assume(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); __VERIFIER_assume(___startrek_current_priority_[4] == _i___startrek_current_priority_[5]); break; case 5: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[5] == _i___startrek_job_count_OSEK_Task_ts1_[6]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[5] == _i___startrek_job_count_OSEK_Task_ts2_[6]); __VERIFIER_assume(_trans_[5] == _i_trans_[6]); __VERIFIER_assume(_cmd_turn_[5] == _i_cmd_turn_[6]); __VERIFIER_assume(_cmd_forward_[5] == _i_cmd_forward_[6]); __VERIFIER_assume(_obstacle_flag_[5] == _i_obstacle_flag_[6]); __VERIFIER_assume(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); __VERIFIER_assume(___startrek_current_priority_[5] == _i___startrek_current_priority_[6]); break; case 6: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[6] == _i___startrek_job_count_OSEK_Task_ts1_[7]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[6] == _i___startrek_job_count_OSEK_Task_ts2_[7]); __VERIFIER_assume(_trans_[6] == _i_trans_[7]); __VERIFIER_assume(_cmd_turn_[6] == _i_cmd_turn_[7]); __VERIFIER_assume(_cmd_forward_[6] == _i_cmd_forward_[7]); __VERIFIER_assume(_obstacle_flag_[6] == _i_obstacle_flag_[7]); __VERIFIER_assume(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); __VERIFIER_assume(___startrek_current_priority_[6] == _i___startrek_current_priority_[7]); break; case 7: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[7] == _i___startrek_job_count_OSEK_Task_ts1_[8]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[7] == _i___startrek_job_count_OSEK_Task_ts2_[8]); __VERIFIER_assume(_trans_[7] == _i_trans_[8]); __VERIFIER_assume(_cmd_turn_[7] == _i_cmd_turn_[8]); __VERIFIER_assume(_cmd_forward_[7] == _i_cmd_forward_[8]); __VERIFIER_assume(_obstacle_flag_[7] == _i_obstacle_flag_[8]); __VERIFIER_assume(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); __VERIFIER_assume(___startrek_current_priority_[7] == _i___startrek_current_priority_[8]); break; case 8: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[8] == _i___startrek_job_count_OSEK_Task_ts1_[9]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[8] == _i___startrek_job_count_OSEK_Task_ts2_[9]); __VERIFIER_assume(_trans_[8] == _i_trans_[9]); __VERIFIER_assume(_cmd_turn_[8] == _i_cmd_turn_[9]); __VERIFIER_assume(_cmd_forward_[8] == _i_cmd_forward_[9]); __VERIFIER_assume(_obstacle_flag_[8] == _i_obstacle_flag_[9]); __VERIFIER_assume(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); __VERIFIER_assume(___startrek_current_priority_[8] == _i___startrek_current_priority_[9]); break; case 9: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[9] == _i___startrek_job_count_OSEK_Task_ts1_[10]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[9] == _i___startrek_job_count_OSEK_Task_ts2_[10]); __VERIFIER_assume(_trans_[9] == _i_trans_[10]); __VERIFIER_assume(_cmd_turn_[9] == _i_cmd_turn_[10]); __VERIFIER_assume(_cmd_forward_[9] == _i_cmd_forward_[10]); __VERIFIER_assume(_obstacle_flag_[9] == _i_obstacle_flag_[10]); __VERIFIER_assume(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); __VERIFIER_assume(___startrek_current_priority_[9] == _i___startrek_current_priority_[10]); break; case 10: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[10] == _i___startrek_job_count_OSEK_Task_ts1_[11]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[10] == _i___startrek_job_count_OSEK_Task_ts2_[11]); __VERIFIER_assume(_trans_[10] == _i_trans_[11]); __VERIFIER_assume(_cmd_turn_[10] == _i_cmd_turn_[11]); __VERIFIER_assume(_cmd_forward_[10] == _i_cmd_forward_[11]); __VERIFIER_assume(_obstacle_flag_[10] == _i_obstacle_flag_[11]); __VERIFIER_assume(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); __VERIFIER_assume(___startrek_current_priority_[10] == _i___startrek_current_priority_[11]); break; case 11: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[11] == _i___startrek_job_count_OSEK_Task_ts1_[12]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[11] == _i___startrek_job_count_OSEK_Task_ts2_[12]); __VERIFIER_assume(_trans_[11] == _i_trans_[12]); __VERIFIER_assume(_cmd_turn_[11] == _i_cmd_turn_[12]); __VERIFIER_assume(_cmd_forward_[11] == _i_cmd_forward_[12]); __VERIFIER_assume(_obstacle_flag_[11] == _i_obstacle_flag_[12]); __VERIFIER_assume(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); __VERIFIER_assume(___startrek_current_priority_[11] == _i___startrek_current_priority_[12]); break; case 12: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[12] == _i___startrek_job_count_OSEK_Task_ts1_[13]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[12] == _i___startrek_job_count_OSEK_Task_ts2_[13]); __VERIFIER_assume(_trans_[12] == _i_trans_[13]); __VERIFIER_assume(_cmd_turn_[12] == _i_cmd_turn_[13]); __VERIFIER_assume(_cmd_forward_[12] == _i_cmd_forward_[13]); __VERIFIER_assume(_obstacle_flag_[12] == _i_obstacle_flag_[13]); __VERIFIER_assume(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); __VERIFIER_assume(___startrek_current_priority_[12] == _i___startrek_current_priority_[13]); break; case 13: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[13] == _i___startrek_job_count_OSEK_Task_ts1_[14]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[13] == _i___startrek_job_count_OSEK_Task_ts2_[14]); __VERIFIER_assume(_trans_[13] == _i_trans_[14]); __VERIFIER_assume(_cmd_turn_[13] == _i_cmd_turn_[14]); __VERIFIER_assume(_cmd_forward_[13] == _i_cmd_forward_[14]); __VERIFIER_assume(_obstacle_flag_[13] == _i_obstacle_flag_[14]); __VERIFIER_assume(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); __VERIFIER_assume(___startrek_current_priority_[13] == _i___startrek_current_priority_[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_ts3(); __VERIFIER_assume(__startrek_round == __startrek_job_end); switch (__startrek_job_end) { case 0: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[0] == _i___startrek_job_count_OSEK_Task_ts1_[1]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[0] == _i___startrek_job_count_OSEK_Task_ts2_[1]); __VERIFIER_assume(_trans_[0] == _i_trans_[1]); __VERIFIER_assume(_cmd_turn_[0] == _i_cmd_turn_[1]); __VERIFIER_assume(_cmd_forward_[0] == _i_cmd_forward_[1]); __VERIFIER_assume(_obstacle_flag_[0] == _i_obstacle_flag_[1]); __VERIFIER_assume(_nxtway_gs_mode_[0] == _i_nxtway_gs_mode_[1]); __VERIFIER_assume(___startrek_current_priority_[0] == _i___startrek_current_priority_[1]); break; case 1: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[1] == _i___startrek_job_count_OSEK_Task_ts1_[2]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[1] == _i___startrek_job_count_OSEK_Task_ts2_[2]); __VERIFIER_assume(_trans_[1] == _i_trans_[2]); __VERIFIER_assume(_cmd_turn_[1] == _i_cmd_turn_[2]); __VERIFIER_assume(_cmd_forward_[1] == _i_cmd_forward_[2]); __VERIFIER_assume(_obstacle_flag_[1] == _i_obstacle_flag_[2]); __VERIFIER_assume(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); __VERIFIER_assume(___startrek_current_priority_[1] == _i___startrek_current_priority_[2]); break; case 2: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[2] == _i___startrek_job_count_OSEK_Task_ts1_[3]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[2] == _i___startrek_job_count_OSEK_Task_ts2_[3]); __VERIFIER_assume(_trans_[2] == _i_trans_[3]); __VERIFIER_assume(_cmd_turn_[2] == _i_cmd_turn_[3]); __VERIFIER_assume(_cmd_forward_[2] == _i_cmd_forward_[3]); __VERIFIER_assume(_obstacle_flag_[2] == _i_obstacle_flag_[3]); __VERIFIER_assume(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); __VERIFIER_assume(___startrek_current_priority_[2] == _i___startrek_current_priority_[3]); break; case 3: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[3] == _i___startrek_job_count_OSEK_Task_ts1_[4]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[3] == _i___startrek_job_count_OSEK_Task_ts2_[4]); __VERIFIER_assume(_trans_[3] == _i_trans_[4]); __VERIFIER_assume(_cmd_turn_[3] == _i_cmd_turn_[4]); __VERIFIER_assume(_cmd_forward_[3] == _i_cmd_forward_[4]); __VERIFIER_assume(_obstacle_flag_[3] == _i_obstacle_flag_[4]); __VERIFIER_assume(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); __VERIFIER_assume(___startrek_current_priority_[3] == _i___startrek_current_priority_[4]); break; case 4: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[4] == _i___startrek_job_count_OSEK_Task_ts1_[5]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[4] == _i___startrek_job_count_OSEK_Task_ts2_[5]); __VERIFIER_assume(_trans_[4] == _i_trans_[5]); __VERIFIER_assume(_cmd_turn_[4] == _i_cmd_turn_[5]); __VERIFIER_assume(_cmd_forward_[4] == _i_cmd_forward_[5]); __VERIFIER_assume(_obstacle_flag_[4] == _i_obstacle_flag_[5]); __VERIFIER_assume(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); __VERIFIER_assume(___startrek_current_priority_[4] == _i___startrek_current_priority_[5]); break; case 5: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[5] == _i___startrek_job_count_OSEK_Task_ts1_[6]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[5] == _i___startrek_job_count_OSEK_Task_ts2_[6]); __VERIFIER_assume(_trans_[5] == _i_trans_[6]); __VERIFIER_assume(_cmd_turn_[5] == _i_cmd_turn_[6]); __VERIFIER_assume(_cmd_forward_[5] == _i_cmd_forward_[6]); __VERIFIER_assume(_obstacle_flag_[5] == _i_obstacle_flag_[6]); __VERIFIER_assume(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); __VERIFIER_assume(___startrek_current_priority_[5] == _i___startrek_current_priority_[6]); break; case 6: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[6] == _i___startrek_job_count_OSEK_Task_ts1_[7]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[6] == _i___startrek_job_count_OSEK_Task_ts2_[7]); __VERIFIER_assume(_trans_[6] == _i_trans_[7]); __VERIFIER_assume(_cmd_turn_[6] == _i_cmd_turn_[7]); __VERIFIER_assume(_cmd_forward_[6] == _i_cmd_forward_[7]); __VERIFIER_assume(_obstacle_flag_[6] == _i_obstacle_flag_[7]); __VERIFIER_assume(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); __VERIFIER_assume(___startrek_current_priority_[6] == _i___startrek_current_priority_[7]); break; case 7: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[7] == _i___startrek_job_count_OSEK_Task_ts1_[8]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[7] == _i___startrek_job_count_OSEK_Task_ts2_[8]); __VERIFIER_assume(_trans_[7] == _i_trans_[8]); __VERIFIER_assume(_cmd_turn_[7] == _i_cmd_turn_[8]); __VERIFIER_assume(_cmd_forward_[7] == _i_cmd_forward_[8]); __VERIFIER_assume(_obstacle_flag_[7] == _i_obstacle_flag_[8]); __VERIFIER_assume(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); __VERIFIER_assume(___startrek_current_priority_[7] == _i___startrek_current_priority_[8]); break; case 8: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[8] == _i___startrek_job_count_OSEK_Task_ts1_[9]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[8] == _i___startrek_job_count_OSEK_Task_ts2_[9]); __VERIFIER_assume(_trans_[8] == _i_trans_[9]); __VERIFIER_assume(_cmd_turn_[8] == _i_cmd_turn_[9]); __VERIFIER_assume(_cmd_forward_[8] == _i_cmd_forward_[9]); __VERIFIER_assume(_obstacle_flag_[8] == _i_obstacle_flag_[9]); __VERIFIER_assume(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); __VERIFIER_assume(___startrek_current_priority_[8] == _i___startrek_current_priority_[9]); break; case 9: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[9] == _i___startrek_job_count_OSEK_Task_ts1_[10]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[9] == _i___startrek_job_count_OSEK_Task_ts2_[10]); __VERIFIER_assume(_trans_[9] == _i_trans_[10]); __VERIFIER_assume(_cmd_turn_[9] == _i_cmd_turn_[10]); __VERIFIER_assume(_cmd_forward_[9] == _i_cmd_forward_[10]); __VERIFIER_assume(_obstacle_flag_[9] == _i_obstacle_flag_[10]); __VERIFIER_assume(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); __VERIFIER_assume(___startrek_current_priority_[9] == _i___startrek_current_priority_[10]); break; case 10: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[10] == _i___startrek_job_count_OSEK_Task_ts1_[11]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[10] == _i___startrek_job_count_OSEK_Task_ts2_[11]); __VERIFIER_assume(_trans_[10] == _i_trans_[11]); __VERIFIER_assume(_cmd_turn_[10] == _i_cmd_turn_[11]); __VERIFIER_assume(_cmd_forward_[10] == _i_cmd_forward_[11]); __VERIFIER_assume(_obstacle_flag_[10] == _i_obstacle_flag_[11]); __VERIFIER_assume(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); __VERIFIER_assume(___startrek_current_priority_[10] == _i___startrek_current_priority_[11]); break; case 11: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[11] == _i___startrek_job_count_OSEK_Task_ts1_[12]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[11] == _i___startrek_job_count_OSEK_Task_ts2_[12]); __VERIFIER_assume(_trans_[11] == _i_trans_[12]); __VERIFIER_assume(_cmd_turn_[11] == _i_cmd_turn_[12]); __VERIFIER_assume(_cmd_forward_[11] == _i_cmd_forward_[12]); __VERIFIER_assume(_obstacle_flag_[11] == _i_obstacle_flag_[12]); __VERIFIER_assume(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); __VERIFIER_assume(___startrek_current_priority_[11] == _i___startrek_current_priority_[12]); break; case 12: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[12] == _i___startrek_job_count_OSEK_Task_ts1_[13]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[12] == _i___startrek_job_count_OSEK_Task_ts2_[13]); __VERIFIER_assume(_trans_[12] == _i_trans_[13]); __VERIFIER_assume(_cmd_turn_[12] == _i_cmd_turn_[13]); __VERIFIER_assume(_cmd_forward_[12] == _i_cmd_forward_[13]); __VERIFIER_assume(_obstacle_flag_[12] == _i_obstacle_flag_[13]); __VERIFIER_assume(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); __VERIFIER_assume(___startrek_current_priority_[12] == _i___startrek_current_priority_[13]); break; case 13: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[13] == _i___startrek_job_count_OSEK_Task_ts1_[14]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[13] == _i___startrek_job_count_OSEK_Task_ts2_[14]); __VERIFIER_assume(_trans_[13] == _i_trans_[14]); __VERIFIER_assume(_cmd_turn_[13] == _i_cmd_turn_[14]); __VERIFIER_assume(_cmd_forward_[13] == _i_cmd_forward_[14]); __VERIFIER_assume(_obstacle_flag_[13] == _i_obstacle_flag_[14]); __VERIFIER_assume(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); __VERIFIER_assume(___startrek_current_priority_[13] == _i___startrek_current_priority_[14]); break; case 14: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[14] == _i___startrek_job_count_OSEK_Task_ts1_[15]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[14] == _i___startrek_job_count_OSEK_Task_ts2_[15]); __VERIFIER_assume(_trans_[14] == _i_trans_[15]); __VERIFIER_assume(_cmd_turn_[14] == _i_cmd_turn_[15]); __VERIFIER_assume(_cmd_forward_[14] == _i_cmd_forward_[15]); __VERIFIER_assume(_obstacle_flag_[14] == _i_obstacle_flag_[15]); __VERIFIER_assume(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); __VERIFIER_assume(___startrek_current_priority_[14] == _i___startrek_current_priority_[15]); break; case 15: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[15] == _i___startrek_job_count_OSEK_Task_ts1_[16]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[15] == _i___startrek_job_count_OSEK_Task_ts2_[16]); __VERIFIER_assume(_trans_[15] == _i_trans_[16]); __VERIFIER_assume(_cmd_turn_[15] == _i_cmd_turn_[16]); __VERIFIER_assume(_cmd_forward_[15] == _i_cmd_forward_[16]); __VERIFIER_assume(_obstacle_flag_[15] == _i_obstacle_flag_[16]); __VERIFIER_assume(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); __VERIFIER_assume(___startrek_current_priority_[15] == _i___startrek_current_priority_[16]); break; case 16: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[16] == _i___startrek_job_count_OSEK_Task_ts1_[17]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[16] == _i___startrek_job_count_OSEK_Task_ts2_[17]); __VERIFIER_assume(_trans_[16] == _i_trans_[17]); __VERIFIER_assume(_cmd_turn_[16] == _i_cmd_turn_[17]); __VERIFIER_assume(_cmd_forward_[16] == _i_cmd_forward_[17]); __VERIFIER_assume(_obstacle_flag_[16] == _i_obstacle_flag_[17]); __VERIFIER_assume(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); __VERIFIER_assume(___startrek_current_priority_[16] == _i___startrek_current_priority_[17]); break; case 17: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[17] == _i___startrek_job_count_OSEK_Task_ts1_[18]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[17] == _i___startrek_job_count_OSEK_Task_ts2_[18]); __VERIFIER_assume(_trans_[17] == _i_trans_[18]); __VERIFIER_assume(_cmd_turn_[17] == _i_cmd_turn_[18]); __VERIFIER_assume(_cmd_forward_[17] == _i_cmd_forward_[18]); __VERIFIER_assume(_obstacle_flag_[17] == _i_obstacle_flag_[18]); __VERIFIER_assume(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); __VERIFIER_assume(___startrek_current_priority_[17] == _i___startrek_current_priority_[18]); break; case 18: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[18] == _i___startrek_job_count_OSEK_Task_ts1_[19]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[18] == _i___startrek_job_count_OSEK_Task_ts2_[19]); __VERIFIER_assume(_trans_[18] == _i_trans_[19]); __VERIFIER_assume(_cmd_turn_[18] == _i_cmd_turn_[19]); __VERIFIER_assume(_cmd_forward_[18] == _i_cmd_forward_[19]); __VERIFIER_assume(_obstacle_flag_[18] == _i_obstacle_flag_[19]); __VERIFIER_assume(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); __VERIFIER_assume(___startrek_current_priority_[18] == _i___startrek_current_priority_[19]); break; case 19: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[19] == _i___startrek_job_count_OSEK_Task_ts1_[20]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[19] == _i___startrek_job_count_OSEK_Task_ts2_[20]); __VERIFIER_assume(_trans_[19] == _i_trans_[20]); __VERIFIER_assume(_cmd_turn_[19] == _i_cmd_turn_[20]); __VERIFIER_assume(_cmd_forward_[19] == _i_cmd_forward_[20]); __VERIFIER_assume(_obstacle_flag_[19] == _i_obstacle_flag_[20]); __VERIFIER_assume(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); __VERIFIER_assume(___startrek_current_priority_[19] == _i___startrek_current_priority_[20]); break; case 20: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[20] == _i___startrek_job_count_OSEK_Task_ts1_[21]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[20] == _i___startrek_job_count_OSEK_Task_ts2_[21]); __VERIFIER_assume(_trans_[20] == _i_trans_[21]); __VERIFIER_assume(_cmd_turn_[20] == _i_cmd_turn_[21]); __VERIFIER_assume(_cmd_forward_[20] == _i_cmd_forward_[21]); __VERIFIER_assume(_obstacle_flag_[20] == _i_obstacle_flag_[21]); __VERIFIER_assume(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); __VERIFIER_assume(___startrek_current_priority_[20] == _i___startrek_current_priority_[21]); break; case 21: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[21] == _i___startrek_job_count_OSEK_Task_ts1_[22]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[21] == _i___startrek_job_count_OSEK_Task_ts2_[22]); __VERIFIER_assume(_trans_[21] == _i_trans_[22]); __VERIFIER_assume(_cmd_turn_[21] == _i_cmd_turn_[22]); __VERIFIER_assume(_cmd_forward_[21] == _i_cmd_forward_[22]); __VERIFIER_assume(_obstacle_flag_[21] == _i_obstacle_flag_[22]); __VERIFIER_assume(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); __VERIFIER_assume(___startrek_current_priority_[21] == _i___startrek_current_priority_[22]); break; case 22: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[22] == _i___startrek_job_count_OSEK_Task_ts1_[23]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[22] == _i___startrek_job_count_OSEK_Task_ts2_[23]); __VERIFIER_assume(_trans_[22] == _i_trans_[23]); __VERIFIER_assume(_cmd_turn_[22] == _i_cmd_turn_[23]); __VERIFIER_assume(_cmd_forward_[22] == _i_cmd_forward_[23]); __VERIFIER_assume(_obstacle_flag_[22] == _i_obstacle_flag_[23]); __VERIFIER_assume(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); __VERIFIER_assume(___startrek_current_priority_[22] == _i___startrek_current_priority_[23]); break; case 23: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[23] == _i___startrek_job_count_OSEK_Task_ts1_[24]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[23] == _i___startrek_job_count_OSEK_Task_ts2_[24]); __VERIFIER_assume(_trans_[23] == _i_trans_[24]); __VERIFIER_assume(_cmd_turn_[23] == _i_cmd_turn_[24]); __VERIFIER_assume(_cmd_forward_[23] == _i_cmd_forward_[24]); __VERIFIER_assume(_obstacle_flag_[23] == _i_obstacle_flag_[24]); __VERIFIER_assume(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); __VERIFIER_assume(___startrek_current_priority_[23] == _i___startrek_current_priority_[24]); break; case 24: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[24] == _i___startrek_job_count_OSEK_Task_ts1_[25]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[24] == _i___startrek_job_count_OSEK_Task_ts2_[25]); __VERIFIER_assume(_trans_[24] == _i_trans_[25]); __VERIFIER_assume(_cmd_turn_[24] == _i_cmd_turn_[25]); __VERIFIER_assume(_cmd_forward_[24] == _i_cmd_forward_[25]); __VERIFIER_assume(_obstacle_flag_[24] == _i_obstacle_flag_[25]); __VERIFIER_assume(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); __VERIFIER_assume(___startrek_current_priority_[24] == _i___startrek_current_priority_[25]); break; case 25: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[25] == _i___startrek_job_count_OSEK_Task_ts1_[26]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[25] == _i___startrek_job_count_OSEK_Task_ts2_[26]); __VERIFIER_assume(_trans_[25] == _i_trans_[26]); __VERIFIER_assume(_cmd_turn_[25] == _i_cmd_turn_[26]); __VERIFIER_assume(_cmd_forward_[25] == _i_cmd_forward_[26]); __VERIFIER_assume(_obstacle_flag_[25] == _i_obstacle_flag_[26]); __VERIFIER_assume(_nxtway_gs_mode_[25] == _i_nxtway_gs_mode_[26]); __VERIFIER_assume(___startrek_current_priority_[25] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[1] == _i___startrek_job_count_OSEK_Task_ts1_[2]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[1] == _i___startrek_job_count_OSEK_Task_ts2_[2]); __VERIFIER_assume(_trans_[1] == _i_trans_[2]); __VERIFIER_assume(_cmd_turn_[1] == _i_cmd_turn_[2]); __VERIFIER_assume(_cmd_forward_[1] == _i_cmd_forward_[2]); __VERIFIER_assume(_obstacle_flag_[1] == _i_obstacle_flag_[2]); __VERIFIER_assume(_nxtway_gs_mode_[1] == _i_nxtway_gs_mode_[2]); __VERIFIER_assume(___startrek_current_priority_[1] == _i___startrek_current_priority_[2]); break; case 2: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[2] == _i___startrek_job_count_OSEK_Task_ts1_[3]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[2] == _i___startrek_job_count_OSEK_Task_ts2_[3]); __VERIFIER_assume(_trans_[2] == _i_trans_[3]); __VERIFIER_assume(_cmd_turn_[2] == _i_cmd_turn_[3]); __VERIFIER_assume(_cmd_forward_[2] == _i_cmd_forward_[3]); __VERIFIER_assume(_obstacle_flag_[2] == _i_obstacle_flag_[3]); __VERIFIER_assume(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); __VERIFIER_assume(___startrek_current_priority_[2] == _i___startrek_current_priority_[3]); break; case 3: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[3] == _i___startrek_job_count_OSEK_Task_ts1_[4]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[3] == _i___startrek_job_count_OSEK_Task_ts2_[4]); __VERIFIER_assume(_trans_[3] == _i_trans_[4]); __VERIFIER_assume(_cmd_turn_[3] == _i_cmd_turn_[4]); __VERIFIER_assume(_cmd_forward_[3] == _i_cmd_forward_[4]); __VERIFIER_assume(_obstacle_flag_[3] == _i_obstacle_flag_[4]); __VERIFIER_assume(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); __VERIFIER_assume(___startrek_current_priority_[3] == _i___startrek_current_priority_[4]); break; } assert(__startrek_Assert_t2_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(___startrek_job_count_OSEK_Task_ts1_[2] == _i___startrek_job_count_OSEK_Task_ts1_[3]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[2] == _i___startrek_job_count_OSEK_Task_ts2_[3]); __VERIFIER_assume(_trans_[2] == _i_trans_[3]); __VERIFIER_assume(_cmd_turn_[2] == _i_cmd_turn_[3]); __VERIFIER_assume(_cmd_forward_[2] == _i_cmd_forward_[3]); __VERIFIER_assume(_obstacle_flag_[2] == _i_obstacle_flag_[3]); __VERIFIER_assume(_nxtway_gs_mode_[2] == _i_nxtway_gs_mode_[3]); __VERIFIER_assume(___startrek_current_priority_[2] == _i___startrek_current_priority_[3]); break; case 3: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[3] == _i___startrek_job_count_OSEK_Task_ts1_[4]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[3] == _i___startrek_job_count_OSEK_Task_ts2_[4]); __VERIFIER_assume(_trans_[3] == _i_trans_[4]); __VERIFIER_assume(_cmd_turn_[3] == _i_cmd_turn_[4]); __VERIFIER_assume(_cmd_forward_[3] == _i_cmd_forward_[4]); __VERIFIER_assume(_obstacle_flag_[3] == _i_obstacle_flag_[4]); __VERIFIER_assume(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); __VERIFIER_assume(___startrek_current_priority_[3] == _i___startrek_current_priority_[4]); break; case 4: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[4] == _i___startrek_job_count_OSEK_Task_ts1_[5]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[4] == _i___startrek_job_count_OSEK_Task_ts2_[5]); __VERIFIER_assume(_trans_[4] == _i_trans_[5]); __VERIFIER_assume(_cmd_turn_[4] == _i_cmd_turn_[5]); __VERIFIER_assume(_cmd_forward_[4] == _i_cmd_forward_[5]); __VERIFIER_assume(_obstacle_flag_[4] == _i_obstacle_flag_[5]); __VERIFIER_assume(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); __VERIFIER_assume(___startrek_current_priority_[4] == _i___startrek_current_priority_[5]); break; } assert(__startrek_Assert_t2_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(___startrek_job_count_OSEK_Task_ts1_[3] == _i___startrek_job_count_OSEK_Task_ts1_[4]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[3] == _i___startrek_job_count_OSEK_Task_ts2_[4]); __VERIFIER_assume(_trans_[3] == _i_trans_[4]); __VERIFIER_assume(_cmd_turn_[3] == _i_cmd_turn_[4]); __VERIFIER_assume(_cmd_forward_[3] == _i_cmd_forward_[4]); __VERIFIER_assume(_obstacle_flag_[3] == _i_obstacle_flag_[4]); __VERIFIER_assume(_nxtway_gs_mode_[3] == _i_nxtway_gs_mode_[4]); __VERIFIER_assume(___startrek_current_priority_[3] == _i___startrek_current_priority_[4]); break; case 4: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[4] == _i___startrek_job_count_OSEK_Task_ts1_[5]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[4] == _i___startrek_job_count_OSEK_Task_ts2_[5]); __VERIFIER_assume(_trans_[4] == _i_trans_[5]); __VERIFIER_assume(_cmd_turn_[4] == _i_cmd_turn_[5]); __VERIFIER_assume(_cmd_forward_[4] == _i_cmd_forward_[5]); __VERIFIER_assume(_obstacle_flag_[4] == _i_obstacle_flag_[5]); __VERIFIER_assume(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); __VERIFIER_assume(___startrek_current_priority_[4] == _i___startrek_current_priority_[5]); break; case 5: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[5] == _i___startrek_job_count_OSEK_Task_ts1_[6]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[5] == _i___startrek_job_count_OSEK_Task_ts2_[6]); __VERIFIER_assume(_trans_[5] == _i_trans_[6]); __VERIFIER_assume(_cmd_turn_[5] == _i_cmd_turn_[6]); __VERIFIER_assume(_cmd_forward_[5] == _i_cmd_forward_[6]); __VERIFIER_assume(_obstacle_flag_[5] == _i_obstacle_flag_[6]); __VERIFIER_assume(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); __VERIFIER_assume(___startrek_current_priority_[5] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[4] == _i___startrek_job_count_OSEK_Task_ts1_[5]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[4] == _i___startrek_job_count_OSEK_Task_ts2_[5]); __VERIFIER_assume(_trans_[4] == _i_trans_[5]); __VERIFIER_assume(_cmd_turn_[4] == _i_cmd_turn_[5]); __VERIFIER_assume(_cmd_forward_[4] == _i_cmd_forward_[5]); __VERIFIER_assume(_obstacle_flag_[4] == _i_obstacle_flag_[5]); __VERIFIER_assume(_nxtway_gs_mode_[4] == _i_nxtway_gs_mode_[5]); __VERIFIER_assume(___startrek_current_priority_[4] == _i___startrek_current_priority_[5]); break; case 5: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[5] == _i___startrek_job_count_OSEK_Task_ts1_[6]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[5] == _i___startrek_job_count_OSEK_Task_ts2_[6]); __VERIFIER_assume(_trans_[5] == _i_trans_[6]); __VERIFIER_assume(_cmd_turn_[5] == _i_cmd_turn_[6]); __VERIFIER_assume(_cmd_forward_[5] == _i_cmd_forward_[6]); __VERIFIER_assume(_obstacle_flag_[5] == _i_obstacle_flag_[6]); __VERIFIER_assume(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); __VERIFIER_assume(___startrek_current_priority_[5] == _i___startrek_current_priority_[6]); break; case 6: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[6] == _i___startrek_job_count_OSEK_Task_ts1_[7]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[6] == _i___startrek_job_count_OSEK_Task_ts2_[7]); __VERIFIER_assume(_trans_[6] == _i_trans_[7]); __VERIFIER_assume(_cmd_turn_[6] == _i_cmd_turn_[7]); __VERIFIER_assume(_cmd_forward_[6] == _i_cmd_forward_[7]); __VERIFIER_assume(_obstacle_flag_[6] == _i_obstacle_flag_[7]); __VERIFIER_assume(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); __VERIFIER_assume(___startrek_current_priority_[6] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[5] == _i___startrek_job_count_OSEK_Task_ts1_[6]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[5] == _i___startrek_job_count_OSEK_Task_ts2_[6]); __VERIFIER_assume(_trans_[5] == _i_trans_[6]); __VERIFIER_assume(_cmd_turn_[5] == _i_cmd_turn_[6]); __VERIFIER_assume(_cmd_forward_[5] == _i_cmd_forward_[6]); __VERIFIER_assume(_obstacle_flag_[5] == _i_obstacle_flag_[6]); __VERIFIER_assume(_nxtway_gs_mode_[5] == _i_nxtway_gs_mode_[6]); __VERIFIER_assume(___startrek_current_priority_[5] == _i___startrek_current_priority_[6]); break; case 6: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[6] == _i___startrek_job_count_OSEK_Task_ts1_[7]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[6] == _i___startrek_job_count_OSEK_Task_ts2_[7]); __VERIFIER_assume(_trans_[6] == _i_trans_[7]); __VERIFIER_assume(_cmd_turn_[6] == _i_cmd_turn_[7]); __VERIFIER_assume(_cmd_forward_[6] == _i_cmd_forward_[7]); __VERIFIER_assume(_obstacle_flag_[6] == _i_obstacle_flag_[7]); __VERIFIER_assume(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); __VERIFIER_assume(___startrek_current_priority_[6] == _i___startrek_current_priority_[7]); break; case 7: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[7] == _i___startrek_job_count_OSEK_Task_ts1_[8]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[7] == _i___startrek_job_count_OSEK_Task_ts2_[8]); __VERIFIER_assume(_trans_[7] == _i_trans_[8]); __VERIFIER_assume(_cmd_turn_[7] == _i_cmd_turn_[8]); __VERIFIER_assume(_cmd_forward_[7] == _i_cmd_forward_[8]); __VERIFIER_assume(_obstacle_flag_[7] == _i_obstacle_flag_[8]); __VERIFIER_assume(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); __VERIFIER_assume(___startrek_current_priority_[7] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[6] == _i___startrek_job_count_OSEK_Task_ts1_[7]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[6] == _i___startrek_job_count_OSEK_Task_ts2_[7]); __VERIFIER_assume(_trans_[6] == _i_trans_[7]); __VERIFIER_assume(_cmd_turn_[6] == _i_cmd_turn_[7]); __VERIFIER_assume(_cmd_forward_[6] == _i_cmd_forward_[7]); __VERIFIER_assume(_obstacle_flag_[6] == _i_obstacle_flag_[7]); __VERIFIER_assume(_nxtway_gs_mode_[6] == _i_nxtway_gs_mode_[7]); __VERIFIER_assume(___startrek_current_priority_[6] == _i___startrek_current_priority_[7]); break; case 7: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[7] == _i___startrek_job_count_OSEK_Task_ts1_[8]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[7] == _i___startrek_job_count_OSEK_Task_ts2_[8]); __VERIFIER_assume(_trans_[7] == _i_trans_[8]); __VERIFIER_assume(_cmd_turn_[7] == _i_cmd_turn_[8]); __VERIFIER_assume(_cmd_forward_[7] == _i_cmd_forward_[8]); __VERIFIER_assume(_obstacle_flag_[7] == _i_obstacle_flag_[8]); __VERIFIER_assume(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); __VERIFIER_assume(___startrek_current_priority_[7] == _i___startrek_current_priority_[8]); break; case 8: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[8] == _i___startrek_job_count_OSEK_Task_ts1_[9]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[8] == _i___startrek_job_count_OSEK_Task_ts2_[9]); __VERIFIER_assume(_trans_[8] == _i_trans_[9]); __VERIFIER_assume(_cmd_turn_[8] == _i_cmd_turn_[9]); __VERIFIER_assume(_cmd_forward_[8] == _i_cmd_forward_[9]); __VERIFIER_assume(_obstacle_flag_[8] == _i_obstacle_flag_[9]); __VERIFIER_assume(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); __VERIFIER_assume(___startrek_current_priority_[8] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[7] == _i___startrek_job_count_OSEK_Task_ts1_[8]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[7] == _i___startrek_job_count_OSEK_Task_ts2_[8]); __VERIFIER_assume(_trans_[7] == _i_trans_[8]); __VERIFIER_assume(_cmd_turn_[7] == _i_cmd_turn_[8]); __VERIFIER_assume(_cmd_forward_[7] == _i_cmd_forward_[8]); __VERIFIER_assume(_obstacle_flag_[7] == _i_obstacle_flag_[8]); __VERIFIER_assume(_nxtway_gs_mode_[7] == _i_nxtway_gs_mode_[8]); __VERIFIER_assume(___startrek_current_priority_[7] == _i___startrek_current_priority_[8]); break; case 8: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[8] == _i___startrek_job_count_OSEK_Task_ts1_[9]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[8] == _i___startrek_job_count_OSEK_Task_ts2_[9]); __VERIFIER_assume(_trans_[8] == _i_trans_[9]); __VERIFIER_assume(_cmd_turn_[8] == _i_cmd_turn_[9]); __VERIFIER_assume(_cmd_forward_[8] == _i_cmd_forward_[9]); __VERIFIER_assume(_obstacle_flag_[8] == _i_obstacle_flag_[9]); __VERIFIER_assume(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); __VERIFIER_assume(___startrek_current_priority_[8] == _i___startrek_current_priority_[9]); break; case 9: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[9] == _i___startrek_job_count_OSEK_Task_ts1_[10]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[9] == _i___startrek_job_count_OSEK_Task_ts2_[10]); __VERIFIER_assume(_trans_[9] == _i_trans_[10]); __VERIFIER_assume(_cmd_turn_[9] == _i_cmd_turn_[10]); __VERIFIER_assume(_cmd_forward_[9] == _i_cmd_forward_[10]); __VERIFIER_assume(_obstacle_flag_[9] == _i_obstacle_flag_[10]); __VERIFIER_assume(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); __VERIFIER_assume(___startrek_current_priority_[9] == _i___startrek_current_priority_[10]); break; } assert(__startrek_Assert_t2_i0); assert(__startrek_Assert_t1_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(___startrek_job_count_OSEK_Task_ts1_[8] == _i___startrek_job_count_OSEK_Task_ts1_[9]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[8] == _i___startrek_job_count_OSEK_Task_ts2_[9]); __VERIFIER_assume(_trans_[8] == _i_trans_[9]); __VERIFIER_assume(_cmd_turn_[8] == _i_cmd_turn_[9]); __VERIFIER_assume(_cmd_forward_[8] == _i_cmd_forward_[9]); __VERIFIER_assume(_obstacle_flag_[8] == _i_obstacle_flag_[9]); __VERIFIER_assume(_nxtway_gs_mode_[8] == _i_nxtway_gs_mode_[9]); __VERIFIER_assume(___startrek_current_priority_[8] == _i___startrek_current_priority_[9]); break; case 9: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[9] == _i___startrek_job_count_OSEK_Task_ts1_[10]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[9] == _i___startrek_job_count_OSEK_Task_ts2_[10]); __VERIFIER_assume(_trans_[9] == _i_trans_[10]); __VERIFIER_assume(_cmd_turn_[9] == _i_cmd_turn_[10]); __VERIFIER_assume(_cmd_forward_[9] == _i_cmd_forward_[10]); __VERIFIER_assume(_obstacle_flag_[9] == _i_obstacle_flag_[10]); __VERIFIER_assume(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); __VERIFIER_assume(___startrek_current_priority_[9] == _i___startrek_current_priority_[10]); break; case 10: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[10] == _i___startrek_job_count_OSEK_Task_ts1_[11]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[10] == _i___startrek_job_count_OSEK_Task_ts2_[11]); __VERIFIER_assume(_trans_[10] == _i_trans_[11]); __VERIFIER_assume(_cmd_turn_[10] == _i_cmd_turn_[11]); __VERIFIER_assume(_cmd_forward_[10] == _i_cmd_forward_[11]); __VERIFIER_assume(_obstacle_flag_[10] == _i_obstacle_flag_[11]); __VERIFIER_assume(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); __VERIFIER_assume(___startrek_current_priority_[10] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[9] == _i___startrek_job_count_OSEK_Task_ts1_[10]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[9] == _i___startrek_job_count_OSEK_Task_ts2_[10]); __VERIFIER_assume(_trans_[9] == _i_trans_[10]); __VERIFIER_assume(_cmd_turn_[9] == _i_cmd_turn_[10]); __VERIFIER_assume(_cmd_forward_[9] == _i_cmd_forward_[10]); __VERIFIER_assume(_obstacle_flag_[9] == _i_obstacle_flag_[10]); __VERIFIER_assume(_nxtway_gs_mode_[9] == _i_nxtway_gs_mode_[10]); __VERIFIER_assume(___startrek_current_priority_[9] == _i___startrek_current_priority_[10]); break; case 10: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[10] == _i___startrek_job_count_OSEK_Task_ts1_[11]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[10] == _i___startrek_job_count_OSEK_Task_ts2_[11]); __VERIFIER_assume(_trans_[10] == _i_trans_[11]); __VERIFIER_assume(_cmd_turn_[10] == _i_cmd_turn_[11]); __VERIFIER_assume(_cmd_forward_[10] == _i_cmd_forward_[11]); __VERIFIER_assume(_obstacle_flag_[10] == _i_obstacle_flag_[11]); __VERIFIER_assume(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); __VERIFIER_assume(___startrek_current_priority_[10] == _i___startrek_current_priority_[11]); break; case 11: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[11] == _i___startrek_job_count_OSEK_Task_ts1_[12]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[11] == _i___startrek_job_count_OSEK_Task_ts2_[12]); __VERIFIER_assume(_trans_[11] == _i_trans_[12]); __VERIFIER_assume(_cmd_turn_[11] == _i_cmd_turn_[12]); __VERIFIER_assume(_cmd_forward_[11] == _i_cmd_forward_[12]); __VERIFIER_assume(_obstacle_flag_[11] == _i_obstacle_flag_[12]); __VERIFIER_assume(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); __VERIFIER_assume(___startrek_current_priority_[11] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[10] == _i___startrek_job_count_OSEK_Task_ts1_[11]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[10] == _i___startrek_job_count_OSEK_Task_ts2_[11]); __VERIFIER_assume(_trans_[10] == _i_trans_[11]); __VERIFIER_assume(_cmd_turn_[10] == _i_cmd_turn_[11]); __VERIFIER_assume(_cmd_forward_[10] == _i_cmd_forward_[11]); __VERIFIER_assume(_obstacle_flag_[10] == _i_obstacle_flag_[11]); __VERIFIER_assume(_nxtway_gs_mode_[10] == _i_nxtway_gs_mode_[11]); __VERIFIER_assume(___startrek_current_priority_[10] == _i___startrek_current_priority_[11]); break; case 11: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[11] == _i___startrek_job_count_OSEK_Task_ts1_[12]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[11] == _i___startrek_job_count_OSEK_Task_ts2_[12]); __VERIFIER_assume(_trans_[11] == _i_trans_[12]); __VERIFIER_assume(_cmd_turn_[11] == _i_cmd_turn_[12]); __VERIFIER_assume(_cmd_forward_[11] == _i_cmd_forward_[12]); __VERIFIER_assume(_obstacle_flag_[11] == _i_obstacle_flag_[12]); __VERIFIER_assume(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); __VERIFIER_assume(___startrek_current_priority_[11] == _i___startrek_current_priority_[12]); break; case 12: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[12] == _i___startrek_job_count_OSEK_Task_ts1_[13]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[12] == _i___startrek_job_count_OSEK_Task_ts2_[13]); __VERIFIER_assume(_trans_[12] == _i_trans_[13]); __VERIFIER_assume(_cmd_turn_[12] == _i_cmd_turn_[13]); __VERIFIER_assume(_cmd_forward_[12] == _i_cmd_forward_[13]); __VERIFIER_assume(_obstacle_flag_[12] == _i_obstacle_flag_[13]); __VERIFIER_assume(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); __VERIFIER_assume(___startrek_current_priority_[12] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[11] == _i___startrek_job_count_OSEK_Task_ts1_[12]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[11] == _i___startrek_job_count_OSEK_Task_ts2_[12]); __VERIFIER_assume(_trans_[11] == _i_trans_[12]); __VERIFIER_assume(_cmd_turn_[11] == _i_cmd_turn_[12]); __VERIFIER_assume(_cmd_forward_[11] == _i_cmd_forward_[12]); __VERIFIER_assume(_obstacle_flag_[11] == _i_obstacle_flag_[12]); __VERIFIER_assume(_nxtway_gs_mode_[11] == _i_nxtway_gs_mode_[12]); __VERIFIER_assume(___startrek_current_priority_[11] == _i___startrek_current_priority_[12]); break; case 12: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[12] == _i___startrek_job_count_OSEK_Task_ts1_[13]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[12] == _i___startrek_job_count_OSEK_Task_ts2_[13]); __VERIFIER_assume(_trans_[12] == _i_trans_[13]); __VERIFIER_assume(_cmd_turn_[12] == _i_cmd_turn_[13]); __VERIFIER_assume(_cmd_forward_[12] == _i_cmd_forward_[13]); __VERIFIER_assume(_obstacle_flag_[12] == _i_obstacle_flag_[13]); __VERIFIER_assume(_nxtway_gs_mode_[12] == _i_nxtway_gs_mode_[13]); __VERIFIER_assume(___startrek_current_priority_[12] == _i___startrek_current_priority_[13]); break; case 13: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[13] == _i___startrek_job_count_OSEK_Task_ts1_[14]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[13] == _i___startrek_job_count_OSEK_Task_ts2_[14]); __VERIFIER_assume(_trans_[13] == _i_trans_[14]); __VERIFIER_assume(_cmd_turn_[13] == _i_cmd_turn_[14]); __VERIFIER_assume(_cmd_forward_[13] == _i_cmd_forward_[14]); __VERIFIER_assume(_obstacle_flag_[13] == _i_obstacle_flag_[14]); __VERIFIER_assume(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); __VERIFIER_assume(___startrek_current_priority_[13] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[13] == _i___startrek_job_count_OSEK_Task_ts1_[14]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[13] == _i___startrek_job_count_OSEK_Task_ts2_[14]); __VERIFIER_assume(_trans_[13] == _i_trans_[14]); __VERIFIER_assume(_cmd_turn_[13] == _i_cmd_turn_[14]); __VERIFIER_assume(_cmd_forward_[13] == _i_cmd_forward_[14]); __VERIFIER_assume(_obstacle_flag_[13] == _i_obstacle_flag_[14]); __VERIFIER_assume(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); __VERIFIER_assume(___startrek_current_priority_[13] == _i___startrek_current_priority_[14]); break; case 14: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[14] == _i___startrek_job_count_OSEK_Task_ts1_[15]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[14] == _i___startrek_job_count_OSEK_Task_ts2_[15]); __VERIFIER_assume(_trans_[14] == _i_trans_[15]); __VERIFIER_assume(_cmd_turn_[14] == _i_cmd_turn_[15]); __VERIFIER_assume(_cmd_forward_[14] == _i_cmd_forward_[15]); __VERIFIER_assume(_obstacle_flag_[14] == _i_obstacle_flag_[15]); __VERIFIER_assume(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); __VERIFIER_assume(___startrek_current_priority_[14] == _i___startrek_current_priority_[15]); break; case 15: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[15] == _i___startrek_job_count_OSEK_Task_ts1_[16]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[15] == _i___startrek_job_count_OSEK_Task_ts2_[16]); __VERIFIER_assume(_trans_[15] == _i_trans_[16]); __VERIFIER_assume(_cmd_turn_[15] == _i_cmd_turn_[16]); __VERIFIER_assume(_cmd_forward_[15] == _i_cmd_forward_[16]); __VERIFIER_assume(_obstacle_flag_[15] == _i_obstacle_flag_[16]); __VERIFIER_assume(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); __VERIFIER_assume(___startrek_current_priority_[15] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[13] == _i___startrek_job_count_OSEK_Task_ts1_[14]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[13] == _i___startrek_job_count_OSEK_Task_ts2_[14]); __VERIFIER_assume(_trans_[13] == _i_trans_[14]); __VERIFIER_assume(_cmd_turn_[13] == _i_cmd_turn_[14]); __VERIFIER_assume(_cmd_forward_[13] == _i_cmd_forward_[14]); __VERIFIER_assume(_obstacle_flag_[13] == _i_obstacle_flag_[14]); __VERIFIER_assume(_nxtway_gs_mode_[13] == _i_nxtway_gs_mode_[14]); __VERIFIER_assume(___startrek_current_priority_[13] == _i___startrek_current_priority_[14]); break; case 14: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[14] == _i___startrek_job_count_OSEK_Task_ts1_[15]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[14] == _i___startrek_job_count_OSEK_Task_ts2_[15]); __VERIFIER_assume(_trans_[14] == _i_trans_[15]); __VERIFIER_assume(_cmd_turn_[14] == _i_cmd_turn_[15]); __VERIFIER_assume(_cmd_forward_[14] == _i_cmd_forward_[15]); __VERIFIER_assume(_obstacle_flag_[14] == _i_obstacle_flag_[15]); __VERIFIER_assume(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); __VERIFIER_assume(___startrek_current_priority_[14] == _i___startrek_current_priority_[15]); break; case 15: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[15] == _i___startrek_job_count_OSEK_Task_ts1_[16]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[15] == _i___startrek_job_count_OSEK_Task_ts2_[16]); __VERIFIER_assume(_trans_[15] == _i_trans_[16]); __VERIFIER_assume(_cmd_turn_[15] == _i_cmd_turn_[16]); __VERIFIER_assume(_cmd_forward_[15] == _i_cmd_forward_[16]); __VERIFIER_assume(_obstacle_flag_[15] == _i_obstacle_flag_[16]); __VERIFIER_assume(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); __VERIFIER_assume(___startrek_current_priority_[15] == _i___startrek_current_priority_[16]); break; case 16: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[16] == _i___startrek_job_count_OSEK_Task_ts1_[17]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[16] == _i___startrek_job_count_OSEK_Task_ts2_[17]); __VERIFIER_assume(_trans_[16] == _i_trans_[17]); __VERIFIER_assume(_cmd_turn_[16] == _i_cmd_turn_[17]); __VERIFIER_assume(_cmd_forward_[16] == _i_cmd_forward_[17]); __VERIFIER_assume(_obstacle_flag_[16] == _i_obstacle_flag_[17]); __VERIFIER_assume(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); __VERIFIER_assume(___startrek_current_priority_[16] == _i___startrek_current_priority_[17]); break; case 17: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[17] == _i___startrek_job_count_OSEK_Task_ts1_[18]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[17] == _i___startrek_job_count_OSEK_Task_ts2_[18]); __VERIFIER_assume(_trans_[17] == _i_trans_[18]); __VERIFIER_assume(_cmd_turn_[17] == _i_cmd_turn_[18]); __VERIFIER_assume(_cmd_forward_[17] == _i_cmd_forward_[18]); __VERIFIER_assume(_obstacle_flag_[17] == _i_obstacle_flag_[18]); __VERIFIER_assume(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); __VERIFIER_assume(___startrek_current_priority_[17] == _i___startrek_current_priority_[18]); break; case 18: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[18] == _i___startrek_job_count_OSEK_Task_ts1_[19]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[18] == _i___startrek_job_count_OSEK_Task_ts2_[19]); __VERIFIER_assume(_trans_[18] == _i_trans_[19]); __VERIFIER_assume(_cmd_turn_[18] == _i_cmd_turn_[19]); __VERIFIER_assume(_cmd_forward_[18] == _i_cmd_forward_[19]); __VERIFIER_assume(_obstacle_flag_[18] == _i_obstacle_flag_[19]); __VERIFIER_assume(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); __VERIFIER_assume(___startrek_current_priority_[18] == _i___startrek_current_priority_[19]); break; case 19: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[19] == _i___startrek_job_count_OSEK_Task_ts1_[20]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[19] == _i___startrek_job_count_OSEK_Task_ts2_[20]); __VERIFIER_assume(_trans_[19] == _i_trans_[20]); __VERIFIER_assume(_cmd_turn_[19] == _i_cmd_turn_[20]); __VERIFIER_assume(_cmd_forward_[19] == _i_cmd_forward_[20]); __VERIFIER_assume(_obstacle_flag_[19] == _i_obstacle_flag_[20]); __VERIFIER_assume(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); __VERIFIER_assume(___startrek_current_priority_[19] == _i___startrek_current_priority_[20]); break; case 20: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[20] == _i___startrek_job_count_OSEK_Task_ts1_[21]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[20] == _i___startrek_job_count_OSEK_Task_ts2_[21]); __VERIFIER_assume(_trans_[20] == _i_trans_[21]); __VERIFIER_assume(_cmd_turn_[20] == _i_cmd_turn_[21]); __VERIFIER_assume(_cmd_forward_[20] == _i_cmd_forward_[21]); __VERIFIER_assume(_obstacle_flag_[20] == _i_obstacle_flag_[21]); __VERIFIER_assume(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); __VERIFIER_assume(___startrek_current_priority_[20] == _i___startrek_current_priority_[21]); break; case 21: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[21] == _i___startrek_job_count_OSEK_Task_ts1_[22]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[21] == _i___startrek_job_count_OSEK_Task_ts2_[22]); __VERIFIER_assume(_trans_[21] == _i_trans_[22]); __VERIFIER_assume(_cmd_turn_[21] == _i_cmd_turn_[22]); __VERIFIER_assume(_cmd_forward_[21] == _i_cmd_forward_[22]); __VERIFIER_assume(_obstacle_flag_[21] == _i_obstacle_flag_[22]); __VERIFIER_assume(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); __VERIFIER_assume(___startrek_current_priority_[21] == _i___startrek_current_priority_[22]); break; case 22: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[22] == _i___startrek_job_count_OSEK_Task_ts1_[23]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[22] == _i___startrek_job_count_OSEK_Task_ts2_[23]); __VERIFIER_assume(_trans_[22] == _i_trans_[23]); __VERIFIER_assume(_cmd_turn_[22] == _i_cmd_turn_[23]); __VERIFIER_assume(_cmd_forward_[22] == _i_cmd_forward_[23]); __VERIFIER_assume(_obstacle_flag_[22] == _i_obstacle_flag_[23]); __VERIFIER_assume(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); __VERIFIER_assume(___startrek_current_priority_[22] == _i___startrek_current_priority_[23]); break; case 23: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[23] == _i___startrek_job_count_OSEK_Task_ts1_[24]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[23] == _i___startrek_job_count_OSEK_Task_ts2_[24]); __VERIFIER_assume(_trans_[23] == _i_trans_[24]); __VERIFIER_assume(_cmd_turn_[23] == _i_cmd_turn_[24]); __VERIFIER_assume(_cmd_forward_[23] == _i_cmd_forward_[24]); __VERIFIER_assume(_obstacle_flag_[23] == _i_obstacle_flag_[24]); __VERIFIER_assume(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); __VERIFIER_assume(___startrek_current_priority_[23] == _i___startrek_current_priority_[24]); break; case 24: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[24] == _i___startrek_job_count_OSEK_Task_ts1_[25]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[24] == _i___startrek_job_count_OSEK_Task_ts2_[25]); __VERIFIER_assume(_trans_[24] == _i_trans_[25]); __VERIFIER_assume(_cmd_turn_[24] == _i_cmd_turn_[25]); __VERIFIER_assume(_cmd_forward_[24] == _i_cmd_forward_[25]); __VERIFIER_assume(_obstacle_flag_[24] == _i_obstacle_flag_[25]); __VERIFIER_assume(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); __VERIFIER_assume(___startrek_current_priority_[24] == _i___startrek_current_priority_[25]); break; case 25: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[25] == _i___startrek_job_count_OSEK_Task_ts1_[26]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[25] == _i___startrek_job_count_OSEK_Task_ts2_[26]); __VERIFIER_assume(_trans_[25] == _i_trans_[26]); __VERIFIER_assume(_cmd_turn_[25] == _i_cmd_turn_[26]); __VERIFIER_assume(_cmd_forward_[25] == _i_cmd_forward_[26]); __VERIFIER_assume(_obstacle_flag_[25] == _i_obstacle_flag_[26]); __VERIFIER_assume(_nxtway_gs_mode_[25] == _i_nxtway_gs_mode_[26]); __VERIFIER_assume(___startrek_current_priority_[25] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[14] == _i___startrek_job_count_OSEK_Task_ts1_[15]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[14] == _i___startrek_job_count_OSEK_Task_ts2_[15]); __VERIFIER_assume(_trans_[14] == _i_trans_[15]); __VERIFIER_assume(_cmd_turn_[14] == _i_cmd_turn_[15]); __VERIFIER_assume(_cmd_forward_[14] == _i_cmd_forward_[15]); __VERIFIER_assume(_obstacle_flag_[14] == _i_obstacle_flag_[15]); __VERIFIER_assume(_nxtway_gs_mode_[14] == _i_nxtway_gs_mode_[15]); __VERIFIER_assume(___startrek_current_priority_[14] == _i___startrek_current_priority_[15]); break; case 15: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[15] == _i___startrek_job_count_OSEK_Task_ts1_[16]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[15] == _i___startrek_job_count_OSEK_Task_ts2_[16]); __VERIFIER_assume(_trans_[15] == _i_trans_[16]); __VERIFIER_assume(_cmd_turn_[15] == _i_cmd_turn_[16]); __VERIFIER_assume(_cmd_forward_[15] == _i_cmd_forward_[16]); __VERIFIER_assume(_obstacle_flag_[15] == _i_obstacle_flag_[16]); __VERIFIER_assume(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); __VERIFIER_assume(___startrek_current_priority_[15] == _i___startrek_current_priority_[16]); break; case 16: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[16] == _i___startrek_job_count_OSEK_Task_ts1_[17]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[16] == _i___startrek_job_count_OSEK_Task_ts2_[17]); __VERIFIER_assume(_trans_[16] == _i_trans_[17]); __VERIFIER_assume(_cmd_turn_[16] == _i_cmd_turn_[17]); __VERIFIER_assume(_cmd_forward_[16] == _i_cmd_forward_[17]); __VERIFIER_assume(_obstacle_flag_[16] == _i_obstacle_flag_[17]); __VERIFIER_assume(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); __VERIFIER_assume(___startrek_current_priority_[16] == _i___startrek_current_priority_[17]); break; } assert(__startrek_Assert_t2_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(___startrek_job_count_OSEK_Task_ts1_[15] == _i___startrek_job_count_OSEK_Task_ts1_[16]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[15] == _i___startrek_job_count_OSEK_Task_ts2_[16]); __VERIFIER_assume(_trans_[15] == _i_trans_[16]); __VERIFIER_assume(_cmd_turn_[15] == _i_cmd_turn_[16]); __VERIFIER_assume(_cmd_forward_[15] == _i_cmd_forward_[16]); __VERIFIER_assume(_obstacle_flag_[15] == _i_obstacle_flag_[16]); __VERIFIER_assume(_nxtway_gs_mode_[15] == _i_nxtway_gs_mode_[16]); __VERIFIER_assume(___startrek_current_priority_[15] == _i___startrek_current_priority_[16]); break; case 16: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[16] == _i___startrek_job_count_OSEK_Task_ts1_[17]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[16] == _i___startrek_job_count_OSEK_Task_ts2_[17]); __VERIFIER_assume(_trans_[16] == _i_trans_[17]); __VERIFIER_assume(_cmd_turn_[16] == _i_cmd_turn_[17]); __VERIFIER_assume(_cmd_forward_[16] == _i_cmd_forward_[17]); __VERIFIER_assume(_obstacle_flag_[16] == _i_obstacle_flag_[17]); __VERIFIER_assume(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); __VERIFIER_assume(___startrek_current_priority_[16] == _i___startrek_current_priority_[17]); break; case 17: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[17] == _i___startrek_job_count_OSEK_Task_ts1_[18]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[17] == _i___startrek_job_count_OSEK_Task_ts2_[18]); __VERIFIER_assume(_trans_[17] == _i_trans_[18]); __VERIFIER_assume(_cmd_turn_[17] == _i_cmd_turn_[18]); __VERIFIER_assume(_cmd_forward_[17] == _i_cmd_forward_[18]); __VERIFIER_assume(_obstacle_flag_[17] == _i_obstacle_flag_[18]); __VERIFIER_assume(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); __VERIFIER_assume(___startrek_current_priority_[17] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[16] == _i___startrek_job_count_OSEK_Task_ts1_[17]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[16] == _i___startrek_job_count_OSEK_Task_ts2_[17]); __VERIFIER_assume(_trans_[16] == _i_trans_[17]); __VERIFIER_assume(_cmd_turn_[16] == _i_cmd_turn_[17]); __VERIFIER_assume(_cmd_forward_[16] == _i_cmd_forward_[17]); __VERIFIER_assume(_obstacle_flag_[16] == _i_obstacle_flag_[17]); __VERIFIER_assume(_nxtway_gs_mode_[16] == _i_nxtway_gs_mode_[17]); __VERIFIER_assume(___startrek_current_priority_[16] == _i___startrek_current_priority_[17]); break; case 17: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[17] == _i___startrek_job_count_OSEK_Task_ts1_[18]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[17] == _i___startrek_job_count_OSEK_Task_ts2_[18]); __VERIFIER_assume(_trans_[17] == _i_trans_[18]); __VERIFIER_assume(_cmd_turn_[17] == _i_cmd_turn_[18]); __VERIFIER_assume(_cmd_forward_[17] == _i_cmd_forward_[18]); __VERIFIER_assume(_obstacle_flag_[17] == _i_obstacle_flag_[18]); __VERIFIER_assume(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); __VERIFIER_assume(___startrek_current_priority_[17] == _i___startrek_current_priority_[18]); break; case 18: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[18] == _i___startrek_job_count_OSEK_Task_ts1_[19]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[18] == _i___startrek_job_count_OSEK_Task_ts2_[19]); __VERIFIER_assume(_trans_[18] == _i_trans_[19]); __VERIFIER_assume(_cmd_turn_[18] == _i_cmd_turn_[19]); __VERIFIER_assume(_cmd_forward_[18] == _i_cmd_forward_[19]); __VERIFIER_assume(_obstacle_flag_[18] == _i_obstacle_flag_[19]); __VERIFIER_assume(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); __VERIFIER_assume(___startrek_current_priority_[18] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[17] == _i___startrek_job_count_OSEK_Task_ts1_[18]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[17] == _i___startrek_job_count_OSEK_Task_ts2_[18]); __VERIFIER_assume(_trans_[17] == _i_trans_[18]); __VERIFIER_assume(_cmd_turn_[17] == _i_cmd_turn_[18]); __VERIFIER_assume(_cmd_forward_[17] == _i_cmd_forward_[18]); __VERIFIER_assume(_obstacle_flag_[17] == _i_obstacle_flag_[18]); __VERIFIER_assume(_nxtway_gs_mode_[17] == _i_nxtway_gs_mode_[18]); __VERIFIER_assume(___startrek_current_priority_[17] == _i___startrek_current_priority_[18]); break; case 18: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[18] == _i___startrek_job_count_OSEK_Task_ts1_[19]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[18] == _i___startrek_job_count_OSEK_Task_ts2_[19]); __VERIFIER_assume(_trans_[18] == _i_trans_[19]); __VERIFIER_assume(_cmd_turn_[18] == _i_cmd_turn_[19]); __VERIFIER_assume(_cmd_forward_[18] == _i_cmd_forward_[19]); __VERIFIER_assume(_obstacle_flag_[18] == _i_obstacle_flag_[19]); __VERIFIER_assume(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); __VERIFIER_assume(___startrek_current_priority_[18] == _i___startrek_current_priority_[19]); break; case 19: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[19] == _i___startrek_job_count_OSEK_Task_ts1_[20]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[19] == _i___startrek_job_count_OSEK_Task_ts2_[20]); __VERIFIER_assume(_trans_[19] == _i_trans_[20]); __VERIFIER_assume(_cmd_turn_[19] == _i_cmd_turn_[20]); __VERIFIER_assume(_cmd_forward_[19] == _i_cmd_forward_[20]); __VERIFIER_assume(_obstacle_flag_[19] == _i_obstacle_flag_[20]); __VERIFIER_assume(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); __VERIFIER_assume(___startrek_current_priority_[19] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[18] == _i___startrek_job_count_OSEK_Task_ts1_[19]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[18] == _i___startrek_job_count_OSEK_Task_ts2_[19]); __VERIFIER_assume(_trans_[18] == _i_trans_[19]); __VERIFIER_assume(_cmd_turn_[18] == _i_cmd_turn_[19]); __VERIFIER_assume(_cmd_forward_[18] == _i_cmd_forward_[19]); __VERIFIER_assume(_obstacle_flag_[18] == _i_obstacle_flag_[19]); __VERIFIER_assume(_nxtway_gs_mode_[18] == _i_nxtway_gs_mode_[19]); __VERIFIER_assume(___startrek_current_priority_[18] == _i___startrek_current_priority_[19]); break; case 19: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[19] == _i___startrek_job_count_OSEK_Task_ts1_[20]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[19] == _i___startrek_job_count_OSEK_Task_ts2_[20]); __VERIFIER_assume(_trans_[19] == _i_trans_[20]); __VERIFIER_assume(_cmd_turn_[19] == _i_cmd_turn_[20]); __VERIFIER_assume(_cmd_forward_[19] == _i_cmd_forward_[20]); __VERIFIER_assume(_obstacle_flag_[19] == _i_obstacle_flag_[20]); __VERIFIER_assume(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); __VERIFIER_assume(___startrek_current_priority_[19] == _i___startrek_current_priority_[20]); break; case 20: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[20] == _i___startrek_job_count_OSEK_Task_ts1_[21]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[20] == _i___startrek_job_count_OSEK_Task_ts2_[21]); __VERIFIER_assume(_trans_[20] == _i_trans_[21]); __VERIFIER_assume(_cmd_turn_[20] == _i_cmd_turn_[21]); __VERIFIER_assume(_cmd_forward_[20] == _i_cmd_forward_[21]); __VERIFIER_assume(_obstacle_flag_[20] == _i_obstacle_flag_[21]); __VERIFIER_assume(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); __VERIFIER_assume(___startrek_current_priority_[20] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[19] == _i___startrek_job_count_OSEK_Task_ts1_[20]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[19] == _i___startrek_job_count_OSEK_Task_ts2_[20]); __VERIFIER_assume(_trans_[19] == _i_trans_[20]); __VERIFIER_assume(_cmd_turn_[19] == _i_cmd_turn_[20]); __VERIFIER_assume(_cmd_forward_[19] == _i_cmd_forward_[20]); __VERIFIER_assume(_obstacle_flag_[19] == _i_obstacle_flag_[20]); __VERIFIER_assume(_nxtway_gs_mode_[19] == _i_nxtway_gs_mode_[20]); __VERIFIER_assume(___startrek_current_priority_[19] == _i___startrek_current_priority_[20]); break; case 20: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[20] == _i___startrek_job_count_OSEK_Task_ts1_[21]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[20] == _i___startrek_job_count_OSEK_Task_ts2_[21]); __VERIFIER_assume(_trans_[20] == _i_trans_[21]); __VERIFIER_assume(_cmd_turn_[20] == _i_cmd_turn_[21]); __VERIFIER_assume(_cmd_forward_[20] == _i_cmd_forward_[21]); __VERIFIER_assume(_obstacle_flag_[20] == _i_obstacle_flag_[21]); __VERIFIER_assume(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); __VERIFIER_assume(___startrek_current_priority_[20] == _i___startrek_current_priority_[21]); break; case 21: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[21] == _i___startrek_job_count_OSEK_Task_ts1_[22]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[21] == _i___startrek_job_count_OSEK_Task_ts2_[22]); __VERIFIER_assume(_trans_[21] == _i_trans_[22]); __VERIFIER_assume(_cmd_turn_[21] == _i_cmd_turn_[22]); __VERIFIER_assume(_cmd_forward_[21] == _i_cmd_forward_[22]); __VERIFIER_assume(_obstacle_flag_[21] == _i_obstacle_flag_[22]); __VERIFIER_assume(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); __VERIFIER_assume(___startrek_current_priority_[21] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[20] == _i___startrek_job_count_OSEK_Task_ts1_[21]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[20] == _i___startrek_job_count_OSEK_Task_ts2_[21]); __VERIFIER_assume(_trans_[20] == _i_trans_[21]); __VERIFIER_assume(_cmd_turn_[20] == _i_cmd_turn_[21]); __VERIFIER_assume(_cmd_forward_[20] == _i_cmd_forward_[21]); __VERIFIER_assume(_obstacle_flag_[20] == _i_obstacle_flag_[21]); __VERIFIER_assume(_nxtway_gs_mode_[20] == _i_nxtway_gs_mode_[21]); __VERIFIER_assume(___startrek_current_priority_[20] == _i___startrek_current_priority_[21]); break; case 21: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[21] == _i___startrek_job_count_OSEK_Task_ts1_[22]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[21] == _i___startrek_job_count_OSEK_Task_ts2_[22]); __VERIFIER_assume(_trans_[21] == _i_trans_[22]); __VERIFIER_assume(_cmd_turn_[21] == _i_cmd_turn_[22]); __VERIFIER_assume(_cmd_forward_[21] == _i_cmd_forward_[22]); __VERIFIER_assume(_obstacle_flag_[21] == _i_obstacle_flag_[22]); __VERIFIER_assume(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); __VERIFIER_assume(___startrek_current_priority_[21] == _i___startrek_current_priority_[22]); break; case 22: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[22] == _i___startrek_job_count_OSEK_Task_ts1_[23]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[22] == _i___startrek_job_count_OSEK_Task_ts2_[23]); __VERIFIER_assume(_trans_[22] == _i_trans_[23]); __VERIFIER_assume(_cmd_turn_[22] == _i_cmd_turn_[23]); __VERIFIER_assume(_cmd_forward_[22] == _i_cmd_forward_[23]); __VERIFIER_assume(_obstacle_flag_[22] == _i_obstacle_flag_[23]); __VERIFIER_assume(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); __VERIFIER_assume(___startrek_current_priority_[22] == _i___startrek_current_priority_[23]); break; } assert(__startrek_Assert_t2_i0); assert(__startrek_Assert_t1_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(___startrek_job_count_OSEK_Task_ts1_[21] == _i___startrek_job_count_OSEK_Task_ts1_[22]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[21] == _i___startrek_job_count_OSEK_Task_ts2_[22]); __VERIFIER_assume(_trans_[21] == _i_trans_[22]); __VERIFIER_assume(_cmd_turn_[21] == _i_cmd_turn_[22]); __VERIFIER_assume(_cmd_forward_[21] == _i_cmd_forward_[22]); __VERIFIER_assume(_obstacle_flag_[21] == _i_obstacle_flag_[22]); __VERIFIER_assume(_nxtway_gs_mode_[21] == _i_nxtway_gs_mode_[22]); __VERIFIER_assume(___startrek_current_priority_[21] == _i___startrek_current_priority_[22]); break; case 22: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[22] == _i___startrek_job_count_OSEK_Task_ts1_[23]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[22] == _i___startrek_job_count_OSEK_Task_ts2_[23]); __VERIFIER_assume(_trans_[22] == _i_trans_[23]); __VERIFIER_assume(_cmd_turn_[22] == _i_cmd_turn_[23]); __VERIFIER_assume(_cmd_forward_[22] == _i_cmd_forward_[23]); __VERIFIER_assume(_obstacle_flag_[22] == _i_obstacle_flag_[23]); __VERIFIER_assume(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); __VERIFIER_assume(___startrek_current_priority_[22] == _i___startrek_current_priority_[23]); break; case 23: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[23] == _i___startrek_job_count_OSEK_Task_ts1_[24]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[23] == _i___startrek_job_count_OSEK_Task_ts2_[24]); __VERIFIER_assume(_trans_[23] == _i_trans_[24]); __VERIFIER_assume(_cmd_turn_[23] == _i_cmd_turn_[24]); __VERIFIER_assume(_cmd_forward_[23] == _i_cmd_forward_[24]); __VERIFIER_assume(_obstacle_flag_[23] == _i_obstacle_flag_[24]); __VERIFIER_assume(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); __VERIFIER_assume(___startrek_current_priority_[23] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[22] == _i___startrek_job_count_OSEK_Task_ts1_[23]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[22] == _i___startrek_job_count_OSEK_Task_ts2_[23]); __VERIFIER_assume(_trans_[22] == _i_trans_[23]); __VERIFIER_assume(_cmd_turn_[22] == _i_cmd_turn_[23]); __VERIFIER_assume(_cmd_forward_[22] == _i_cmd_forward_[23]); __VERIFIER_assume(_obstacle_flag_[22] == _i_obstacle_flag_[23]); __VERIFIER_assume(_nxtway_gs_mode_[22] == _i_nxtway_gs_mode_[23]); __VERIFIER_assume(___startrek_current_priority_[22] == _i___startrek_current_priority_[23]); break; case 23: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[23] == _i___startrek_job_count_OSEK_Task_ts1_[24]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[23] == _i___startrek_job_count_OSEK_Task_ts2_[24]); __VERIFIER_assume(_trans_[23] == _i_trans_[24]); __VERIFIER_assume(_cmd_turn_[23] == _i_cmd_turn_[24]); __VERIFIER_assume(_cmd_forward_[23] == _i_cmd_forward_[24]); __VERIFIER_assume(_obstacle_flag_[23] == _i_obstacle_flag_[24]); __VERIFIER_assume(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); __VERIFIER_assume(___startrek_current_priority_[23] == _i___startrek_current_priority_[24]); break; case 24: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[24] == _i___startrek_job_count_OSEK_Task_ts1_[25]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[24] == _i___startrek_job_count_OSEK_Task_ts2_[25]); __VERIFIER_assume(_trans_[24] == _i_trans_[25]); __VERIFIER_assume(_cmd_turn_[24] == _i_cmd_turn_[25]); __VERIFIER_assume(_cmd_forward_[24] == _i_cmd_forward_[25]); __VERIFIER_assume(_obstacle_flag_[24] == _i_obstacle_flag_[25]); __VERIFIER_assume(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); __VERIFIER_assume(___startrek_current_priority_[24] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[23] == _i___startrek_job_count_OSEK_Task_ts1_[24]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[23] == _i___startrek_job_count_OSEK_Task_ts2_[24]); __VERIFIER_assume(_trans_[23] == _i_trans_[24]); __VERIFIER_assume(_cmd_turn_[23] == _i_cmd_turn_[24]); __VERIFIER_assume(_cmd_forward_[23] == _i_cmd_forward_[24]); __VERIFIER_assume(_obstacle_flag_[23] == _i_obstacle_flag_[24]); __VERIFIER_assume(_nxtway_gs_mode_[23] == _i_nxtway_gs_mode_[24]); __VERIFIER_assume(___startrek_current_priority_[23] == _i___startrek_current_priority_[24]); break; case 24: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[24] == _i___startrek_job_count_OSEK_Task_ts1_[25]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[24] == _i___startrek_job_count_OSEK_Task_ts2_[25]); __VERIFIER_assume(_trans_[24] == _i_trans_[25]); __VERIFIER_assume(_cmd_turn_[24] == _i_cmd_turn_[25]); __VERIFIER_assume(_cmd_forward_[24] == _i_cmd_forward_[25]); __VERIFIER_assume(_obstacle_flag_[24] == _i_obstacle_flag_[25]); __VERIFIER_assume(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); __VERIFIER_assume(___startrek_current_priority_[24] == _i___startrek_current_priority_[25]); break; case 25: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[25] == _i___startrek_job_count_OSEK_Task_ts1_[26]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[25] == _i___startrek_job_count_OSEK_Task_ts2_[26]); __VERIFIER_assume(_trans_[25] == _i_trans_[26]); __VERIFIER_assume(_cmd_turn_[25] == _i_cmd_turn_[26]); __VERIFIER_assume(_cmd_forward_[25] == _i_cmd_forward_[26]); __VERIFIER_assume(_obstacle_flag_[25] == _i_obstacle_flag_[26]); __VERIFIER_assume(_nxtway_gs_mode_[25] == _i_nxtway_gs_mode_[26]); __VERIFIER_assume(___startrek_current_priority_[25] == _i___startrek_current_priority_[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(___startrek_job_count_OSEK_Task_ts1_[24] == _i___startrek_job_count_OSEK_Task_ts1_[25]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[24] == _i___startrek_job_count_OSEK_Task_ts2_[25]); __VERIFIER_assume(_trans_[24] == _i_trans_[25]); __VERIFIER_assume(_cmd_turn_[24] == _i_cmd_turn_[25]); __VERIFIER_assume(_cmd_forward_[24] == _i_cmd_forward_[25]); __VERIFIER_assume(_obstacle_flag_[24] == _i_obstacle_flag_[25]); __VERIFIER_assume(_nxtway_gs_mode_[24] == _i_nxtway_gs_mode_[25]); __VERIFIER_assume(___startrek_current_priority_[24] == _i___startrek_current_priority_[25]); break; case 25: __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts1_[25] == _i___startrek_job_count_OSEK_Task_ts1_[26]); __VERIFIER_assume(___startrek_job_count_OSEK_Task_ts2_[25] == _i___startrek_job_count_OSEK_Task_ts2_[26]); __VERIFIER_assume(_trans_[25] == _i_trans_[26]); __VERIFIER_assume(_cmd_turn_[25] == _i_cmd_turn_[26]); __VERIFIER_assume(_cmd_forward_[25] == _i_cmd_forward_[26]); __VERIFIER_assume(_obstacle_flag_[25] == _i_obstacle_flag_[26]); __VERIFIER_assume(_nxtway_gs_mode_[25] == _i_nxtway_gs_mode_[26]); __VERIFIER_assume(___startrek_current_priority_[25] == _i___startrek_current_priority_[26]); break; } assert(__startrek_Assert_t2_i0); assert(__startrek_Assert_t0_i0); } } int main(void) { { __startrek_init_shared(); __startrek_user_init(); __startrek_hyper_period = 0; __startrek_hyperperiod(); ___startrek_job_count_OSEK_Task_ts1_[0] = ___startrek_job_count_OSEK_Task_ts1_[26]; ___startrek_job_count_OSEK_Task_ts2_[0] = ___startrek_job_count_OSEK_Task_ts2_[26]; _trans_[0] = _trans_[26]; _cmd_turn_[0] = _cmd_turn_[26]; _cmd_forward_[0] = _cmd_forward_[26]; _obstacle_flag_[0] = _obstacle_flag_[26]; _nxtway_gs_mode_[0] = _nxtway_gs_mode_[26]; ___startrek_current_priority_[0] = ___startrek_current_priority_[26]; __startrek_hyper_period = 1; __startrek_hyperperiod(); ___startrek_job_count_OSEK_Task_ts1_[0] = ___startrek_job_count_OSEK_Task_ts1_[26]; ___startrek_job_count_OSEK_Task_ts2_[0] = ___startrek_job_count_OSEK_Task_ts2_[26]; _trans_[0] = _trans_[26]; _cmd_turn_[0] = _cmd_turn_[26]; _cmd_forward_[0] = _cmd_forward_[26]; _obstacle_flag_[0] = _obstacle_flag_[26]; _nxtway_gs_mode_[0] = _nxtway_gs_mode_[26]; ___startrek_current_priority_[0] = ___startrek_current_priority_[26]; __startrek_hyper_period = 2; __startrek_hyperperiod(); ___startrek_job_count_OSEK_Task_ts1_[0] = ___startrek_job_count_OSEK_Task_ts1_[26]; ___startrek_job_count_OSEK_Task_ts2_[0] = ___startrek_job_count_OSEK_Task_ts2_[26]; _trans_[0] = _trans_[26]; _cmd_turn_[0] = _cmd_turn_[26]; _cmd_forward_[0] = _cmd_forward_[26]; _obstacle_flag_[0] = _obstacle_flag_[26]; _nxtway_gs_mode_[0] = _nxtway_gs_mode_[26]; ___startrek_current_priority_[0] = ___startrek_current_priority_[26]; __startrek_hyper_period = 3; __startrek_hyperperiod(); __startrek_user_final(); } return 0; } __inline static char __startrek_read___startrek_current_priority(void) { 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 = ___startrek_current_priority_[__startrek_round]; return (r1); } } __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 char __startrek_read_cmd_forward(void) { 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 = _cmd_forward_[__startrek_round]; return (r1); } } __inline static char __startrek_read_cmd_turn(void) { 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 = _cmd_turn_[__startrek_round]; return (r1); } } __inline static _Bool __startrek_read_trans(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 = _trans_[__startrek_round]; return (r1); } } __inline static char __startrek_read___startrek_job_count_OSEK_Task_ts2(void) { 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 = ___startrek_job_count_OSEK_Task_ts2_[__startrek_round]; return (r1); } } __inline static char __startrek_read___startrek_job_count_OSEK_Task_ts1(void) { 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 = ___startrek_job_count_OSEK_Task_ts1_[__startrek_round]; return (r1); } } __inline static void __startrek_write___startrek_current_priority(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; } ___startrek_current_priority_[__startrek_round] = arg; } } __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_cmd_forward(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; } _cmd_forward_[__startrek_round] = arg; } } __inline static void __startrek_write_cmd_turn(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; } _cmd_turn_[__startrek_round] = arg; } } __inline static void __startrek_write_trans(_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; } _trans_[__startrek_round] = arg; } } __inline static void __startrek_write___startrek_job_count_OSEK_Task_ts2(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; } ___startrek_job_count_OSEK_Task_ts2_[__startrek_round] = arg; } } __inline static void __startrek_write___startrek_job_count_OSEK_Task_ts1(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; } ___startrek_job_count_OSEK_Task_ts1_[__startrek_round] = arg; } } __inline void __startrek_init_shared(void) { { ___startrek_job_count_OSEK_Task_ts1_[0] = __startrek_hidden___startrek_job_count_OSEK_Task_ts1; ___startrek_job_count_OSEK_Task_ts2_[0] = __startrek_hidden___startrek_job_count_OSEK_Task_ts2; _trans_[0] = __startrek_hidden_trans; _cmd_turn_[0] = __startrek_hidden_cmd_turn; _cmd_forward_[0] = __startrek_hidden_cmd_forward; _obstacle_flag_[0] = __startrek_hidden_obstacle_flag; _nxtway_gs_mode_[0] = __startrek_hidden_nxtway_gs_mode; ___startrek_current_priority_[0] = __startrek_hidden___startrek_current_priority; } }