extern void abort(void); extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); void reach_error() { __assert_fail("0", "rekcba_aso.2.M1-2.c", 3, "reach_error"); } // This file is part of the SV-Benchmarks collection of verification tasks: // https://github.com/sosy-lab/sv-benchmarks // // SPDX-FileCopyrightText: 2013 Carnegie Mellon University // SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community // // SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU /* Generated by CIL v. 1.4.0 */ /* print_CIL_Input is true */ _Bool __startrek_Assert_t2_i1[24] = {1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1}; _Bool __startrek_Assert_t1_i1[2] = {1, 1}; _Bool __startrek_Assert_t0_i1[1] = {1}; _Bool __startrek_Assert_t2_i0[24] = {1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1}; _Bool __startrek_Assert_t1_i0[2] = {1, 1}; _Bool __startrek_Assert_t0_i0[1] = {1}; unsigned char __startrek_start_t2[24] ; unsigned char __startrek_end_t2[24] ; unsigned char __startrek_start_t1[2] ; unsigned char __startrek_end_t1[2] ; unsigned char __startrek_start_t0[1] ; unsigned char __startrek_end_t0[1] ; void __startrek_init_shared(void) ; __inline static void __startrek_assert_i1(_Bool arg ) ; __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) ; char __VERIFIER_nondet_char(void) ; _Bool __VERIFIER_nondet_bool(void) ; unsigned char __VERIFIER_nondet_uchar(void) ; _Bool __VERIFIER_nondet_bool(void) ; extern int __VERIFIER_nondet_int(); void abort(void); void assume_abort_if_not(int cond) { if(!cond) {abort();} } unsigned char __startrek_task ; unsigned char __startrek_job ; unsigned char __startrek_job_end ; unsigned char __startrek_error_round ; unsigned char __startrek_round ; _Bool __startrek_lock = (_Bool)0; _Bool __startrek_is_first_cs ; unsigned char __startrek_hyper_period ; #pragma merger(0,"/tmp/aaaa/aso.bug2.i","-S") extern void __startrek_cpu_lock(void) ; extern void __startrek_cpu_unlock(void) ; void assert(_Bool arg) { if (!arg) { ERROR: {reach_error();abort();}} } static unsigned int ud_err_theta ; static unsigned int ud_psi ; static unsigned int ud_theta_lpf ; static unsigned int ud_theta_ref ; static unsigned int ud_thetadot_cmd_lpf ; extern unsigned int A_D ; extern unsigned int A_R ; extern unsigned int K_F[4] ; extern unsigned int K_I ; extern unsigned int K_PHIDOT ; extern unsigned int K_THETADOT ; extern unsigned int const BATTERY_GAIN ; extern unsigned int const BATTERY_OFFSET ; void balance_init(void) { { ud_err_theta = 0.0F; ud_theta_ref = 0.0F; ud_thetadot_cmd_lpf = 0.0F; ud_psi = 0.0F; ud_theta_lpf = 0.0F; return; } } void balance_control(unsigned int args_cmd_forward , unsigned int args_cmd_turn , unsigned int args_gyro , unsigned int args_gyro_offset , unsigned int args_theta_m_l , unsigned int args_theta_m_r , unsigned int args_battery , char *ret_pwm_l , char *ret_pwm_r ) { unsigned int tmp_theta ; unsigned int tmp_theta_lpf ; unsigned int tmp_pwm_r_limiter ; unsigned int tmp_psidot ; unsigned int tmp_pwm_turn ; unsigned int tmp_pwm_l_limiter ; unsigned int tmp_thetadot_cmd_lpf ; unsigned int tmp[4] ; unsigned int tmp_theta_0[4] ; int tmp_0 ; int tmp___0 ; int tmp___1 ; { tmp_thetadot_cmd_lpf = (((float )args_cmd_forward / 100.0F) * (float )K_THETADOT) * (1.0F - (float )A_R) + (float )(A_R * ud_thetadot_cmd_lpf); tmp_theta = ((0.01745329238F * (float )args_theta_m_l + (float )ud_psi) + (0.01745329238F * (float )args_theta_m_r + (float )ud_psi)) * 0.5F; tmp_theta_lpf = (1.0F - (float )A_D) * (float )tmp_theta + (float )(A_D * ud_theta_lpf); tmp_psidot = (float )(args_gyro - args_gyro_offset) * 0.01745329238F; tmp[0] = ud_theta_ref; tmp[1] = 0.0F; tmp[2] = tmp_thetadot_cmd_lpf; tmp[3] = 0.0F; tmp_theta_0[0] = tmp_theta; tmp_theta_0[1] = ud_psi; tmp_theta_0[2] = (float )(tmp_theta_lpf - ud_theta_lpf) / 0.00400000019F; tmp_theta_0[3] = tmp_psidot; tmp_pwm_r_limiter = 0.0F; tmp_0 = 0; tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0]; tmp_0 ++; tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0]; tmp_0 ++; tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0]; tmp_0 ++; tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0]; tmp_0 ++; assume_abort_if_not(((BATTERY_GAIN*args_battery) - BATTERY_OFFSET) != 0); tmp_pwm_r_limiter = (float )((K_I * ud_err_theta + tmp_pwm_r_limiter) / (unsigned int )(BATTERY_GAIN * (unsigned int const )args_battery - BATTERY_OFFSET)) * 100.0F; tmp_pwm_turn = ((float )args_cmd_turn / 100.0F) * (float )K_PHIDOT; tmp_pwm_l_limiter = tmp_pwm_r_limiter + tmp_pwm_turn; tmp___0 = __VERIFIER_nondet_int(); tmp_pwm_l_limiter = tmp___0; *ret_pwm_l = (char )tmp_pwm_l_limiter; tmp_pwm_r_limiter -= tmp_pwm_turn; tmp___1 = __VERIFIER_nondet_int(); tmp_pwm_r_limiter = tmp___1; *ret_pwm_r = (char )tmp_pwm_r_limiter; tmp_pwm_l_limiter = 0.00400000019F * (float )tmp_thetadot_cmd_lpf + (float )ud_theta_ref; tmp_pwm_turn = 0.00400000019F * (float )tmp_psidot + (float )ud_psi; tmp_pwm_r_limiter = (float )(ud_theta_ref - tmp_theta) * 0.00400000019F + (float )ud_err_theta; ud_err_theta = tmp_pwm_r_limiter; ud_theta_ref = tmp_pwm_l_limiter; ud_thetadot_cmd_lpf = tmp_thetadot_cmd_lpf; ud_psi = tmp_pwm_turn; ud_theta_lpf = tmp_theta_lpf; return; } } extern unsigned int __VERIFIER_nondet_uint() ; extern char __VERIFIER_nondet_char() ; extern unsigned char __VERIFIER_nondet_uchar() ; __inline static unsigned char __startrek_read_nxtway_gs_mode(void) ; __inline static void __startrek_write_nxtway_gs_mode(unsigned char arg ) ; unsigned char _nxtway_gs_mode_[27] ; unsigned char _i_nxtway_gs_mode_[27] ; unsigned char __startrek_hidden_nxtway_gs_mode = 0; __inline static _Bool __startrek_read_obstacle_flag(void) ; __inline static void __startrek_write_obstacle_flag(_Bool arg ) ; _Bool _obstacle_flag_[27] ; _Bool _i_obstacle_flag_[27] ; _Bool __startrek_hidden_obstacle_flag = 0; __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; extern void nxt_motor_set_count(unsigned char port , char pwm ) ; char nxt_motor_get_count(unsigned char port ) { char tmp ; { tmp = __VERIFIER_nondet_char(); return (tmp); } } unsigned int ecrobot_get_systick_ms(void) ; static unsigned int timer = 0; unsigned int ecrobot_get_systick_ms(void) { unsigned int r ; { r = timer; timer += 1000U; return (r); } } unsigned int ecrobot_get_gyro_sensor(unsigned char port ) { unsigned int tmp ; { tmp = __VERIFIER_nondet_uint(); return (tmp); } } extern void ecrobot_sound_tone(unsigned int , unsigned int , char ) ; void ecrobot_read_bt_packet(unsigned char *bt_receive_buf , unsigned char sz ) { { *(bt_receive_buf + 0) = __VERIFIER_nondet_uchar(); *(bt_receive_buf + 1) = __VERIFIER_nondet_uchar(); return; } } unsigned int ecrobot_get_battery_voltage(void) { unsigned int tmp ; { tmp = __VERIFIER_nondet_uint(); return (tmp); } } extern void nxt_motor_set_speed(unsigned char port , char speed , char one ) ; extern void ecrobot_bt_data_logger(char , char ) ; static unsigned int gyro_offset ; static unsigned int avg_cnt ; static unsigned int cal_start_time ; void OSEK_Task_ts1(void) { char pwm_l ; char pwm_r ; unsigned char tmp ; unsigned int tmp___0 ; unsigned int tmp___1 ; char tmp___2 ; char tmp___3 ; int tmp___4 ; _Bool tmp___5 ; unsigned int tmp___6 ; char tmp___7 ; char tmp___8 ; unsigned int tmp___9 ; char tmp___10 ; char tmp___11 ; { 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) { assume_abort_if_not(avg_cnt != 0); gyro_offset /= avg_cnt; ecrobot_sound_tone(440U, 500U, 30); __startrek_write_nxtway_gs_mode(2); } break; case 2: tmp___5 = __startrek_read_obstacle_flag(); if (tmp___5) { tmp___2 = __startrek_read_cmd_forward(); if (tmp___2 == -100) { tmp___3 = __startrek_read_cmd_turn(); if (tmp___3 == 0) { tmp___4 = 1; } else { tmp___4 = 0; } } else { tmp___4 = 0; } __startrek_assert_i0(tmp___4); } 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); tmp___10 = __startrek_read_cmd_turn(); tmp___11 = __startrek_read_cmd_forward(); balance_control((unsigned int )tmp___11, (unsigned int )tmp___10, 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_lock = 1; __startrek_write_obstacle_flag(1); __startrek_write_cmd_forward(-100); __startrek_write_cmd_turn(0); __startrek_lock = 0; } } return; } } static unsigned char bt_receive_buf[2] ; void OSEK_Task_ts3(void) { int i ; _Bool wrote ; unsigned char tmp ; _Bool tmp___0 ; int tmp___1 ; _Bool tmp___2 ; char tmp___3 ; char tmp___4 ; { 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; tmp___2 = __startrek_read_obstacle_flag(); if (! tmp___2) { __startrek_write_cmd_forward(- ((int )((char )bt_receive_buf[0]))); __startrek_write_cmd_turn((char )bt_receive_buf[1]); tmp___0 = __startrek_read_obstacle_flag(); if (tmp___0) { tmp___1 = 0; } else { tmp___1 = 1; } __startrek_assert_i1(tmp___1); wrote = 1; } if (wrote) { tmp___3 = __startrek_read_cmd_turn(); tmp___4 = __startrek_read_cmd_forward(); ecrobot_bt_data_logger(tmp___4, tmp___3); } 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 _Bool __startrek_entry_pt_OSEK_Task_ts2(void) ; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts2(void) { { OSEK_Task_ts2(); return ((_Bool)1); } } void cil_keeperOSEK_Task_ts2(void) { { __startrek_entry_pt_OSEK_Task_ts2(); return; } } int __startrek_period_OSEK_Task_ts2 = 48; int __startrek_wcet_OSEK_Task_ts2 = 2; int __startrek_arrival_min_OSEK_Task_ts2 = 0; int __startrek_arrival_max_OSEK_Task_ts2 = 0; char __startrek_base_priority_OSEK_Task_ts1 = 2; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts1(void) ; __inline static _Bool __startrek_entry_pt_OSEK_Task_ts1(void) { { OSEK_Task_ts1(); return ((_Bool)1); } } void cil_keeperOSEK_Task_ts1(void) { { __startrek_entry_pt_OSEK_Task_ts1(); return; } } int __startrek_period_OSEK_Task_ts1 = 4; int __startrek_wcet_OSEK_Task_ts1 = 1; int __startrek_arrival_min_OSEK_Task_ts1 = 0; int __startrek_arrival_max_OSEK_Task_ts1 = 0; int __startrek_time_bound = 96; __inline void __startrek_schedule_jobs(void) { { __startrek_start_t0[0] = __VERIFIER_nondet_uchar(); __startrek_end_t0[0] = __VERIFIER_nondet_uchar(); assume_abort_if_not(0 <= __startrek_start_t0[0]); assume_abort_if_not(__startrek_end_t0[0] <= 26); assume_abort_if_not(__startrek_start_t0[0] <= __startrek_end_t0[0]); __startrek_start_t1[0] = __VERIFIER_nondet_uchar(); __startrek_end_t1[0] = __VERIFIER_nondet_uchar(); __startrek_start_t1[1] = __VERIFIER_nondet_uchar(); __startrek_end_t1[1] = __VERIFIER_nondet_uchar(); assume_abort_if_not(0 <= __startrek_start_t1[0]); assume_abort_if_not(__startrek_end_t1[1] <= 26); assume_abort_if_not(__startrek_start_t1[0] <= __startrek_end_t1[0]); assume_abort_if_not(__startrek_start_t1[1] <= __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t1[0] <= __startrek_start_t1[1] - 1); if (__startrek_start_t0[0] <= __startrek_end_t1[0]) { if (__startrek_start_t1[0] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t1[0]); assume_abort_if_not(__startrek_end_t1[0] < __startrek_end_t0[0]); } } } if (__startrek_start_t0[0] <= __startrek_end_t1[1]) { if (__startrek_start_t1[1] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t1[1]); assume_abort_if_not(__startrek_end_t1[1] < __startrek_end_t0[0]); } } } __startrek_start_t2[0] = __VERIFIER_nondet_uchar(); __startrek_end_t2[0] = __startrek_start_t2[0]; __startrek_start_t2[1] = __VERIFIER_nondet_uchar(); __startrek_end_t2[1] = __startrek_start_t2[1]; __startrek_start_t2[2] = __VERIFIER_nondet_uchar(); __startrek_end_t2[2] = __startrek_start_t2[2]; __startrek_start_t2[3] = __VERIFIER_nondet_uchar(); __startrek_end_t2[3] = __startrek_start_t2[3]; __startrek_start_t2[4] = __VERIFIER_nondet_uchar(); __startrek_end_t2[4] = __startrek_start_t2[4]; __startrek_start_t2[5] = __VERIFIER_nondet_uchar(); __startrek_end_t2[5] = __startrek_start_t2[5]; __startrek_start_t2[6] = __VERIFIER_nondet_uchar(); __startrek_end_t2[6] = __startrek_start_t2[6]; __startrek_start_t2[7] = __VERIFIER_nondet_uchar(); __startrek_end_t2[7] = __startrek_start_t2[7]; __startrek_start_t2[8] = __VERIFIER_nondet_uchar(); __startrek_end_t2[8] = __startrek_start_t2[8]; __startrek_start_t2[9] = __VERIFIER_nondet_uchar(); __startrek_end_t2[9] = __startrek_start_t2[9]; __startrek_start_t2[10] = __VERIFIER_nondet_uchar(); __startrek_end_t2[10] = __startrek_start_t2[10]; __startrek_start_t2[11] = __VERIFIER_nondet_uchar(); __startrek_end_t2[11] = __startrek_start_t2[11]; __startrek_start_t2[12] = __VERIFIER_nondet_uchar(); __startrek_end_t2[12] = __startrek_start_t2[12]; __startrek_start_t2[13] = __VERIFIER_nondet_uchar(); __startrek_end_t2[13] = __startrek_start_t2[13]; __startrek_start_t2[14] = __VERIFIER_nondet_uchar(); __startrek_end_t2[14] = __startrek_start_t2[14]; __startrek_start_t2[15] = __VERIFIER_nondet_uchar(); __startrek_end_t2[15] = __startrek_start_t2[15]; __startrek_start_t2[16] = __VERIFIER_nondet_uchar(); __startrek_end_t2[16] = __startrek_start_t2[16]; __startrek_start_t2[17] = __VERIFIER_nondet_uchar(); __startrek_end_t2[17] = __startrek_start_t2[17]; __startrek_start_t2[18] = __VERIFIER_nondet_uchar(); __startrek_end_t2[18] = __startrek_start_t2[18]; __startrek_start_t2[19] = __VERIFIER_nondet_uchar(); __startrek_end_t2[19] = __startrek_start_t2[19]; __startrek_start_t2[20] = __VERIFIER_nondet_uchar(); __startrek_end_t2[20] = __startrek_start_t2[20]; __startrek_start_t2[21] = __VERIFIER_nondet_uchar(); __startrek_end_t2[21] = __startrek_start_t2[21]; __startrek_start_t2[22] = __VERIFIER_nondet_uchar(); __startrek_end_t2[22] = __startrek_start_t2[22]; __startrek_start_t2[23] = __VERIFIER_nondet_uchar(); __startrek_end_t2[23] = __startrek_start_t2[23]; assume_abort_if_not(0 <= __startrek_start_t2[0]); assume_abort_if_not(__startrek_end_t2[23] <= 26); assume_abort_if_not(__startrek_end_t2[0] <= __startrek_start_t2[1] - 1); assume_abort_if_not(__startrek_end_t2[1] <= __startrek_start_t2[2] - 1); assume_abort_if_not(__startrek_end_t2[2] <= __startrek_start_t2[3] - 1); assume_abort_if_not(__startrek_end_t2[3] <= __startrek_start_t2[4] - 1); assume_abort_if_not(__startrek_end_t2[4] <= __startrek_start_t2[5] - 1); assume_abort_if_not(__startrek_end_t2[5] <= __startrek_start_t2[6] - 1); assume_abort_if_not(__startrek_end_t2[6] <= __startrek_start_t2[7] - 1); assume_abort_if_not(__startrek_end_t2[7] <= __startrek_start_t2[8] - 1); assume_abort_if_not(__startrek_end_t2[8] <= __startrek_start_t2[9] - 1); assume_abort_if_not(__startrek_end_t2[9] <= __startrek_start_t2[10] - 1); assume_abort_if_not(__startrek_end_t2[10] <= __startrek_start_t2[11] - 1); assume_abort_if_not(__startrek_end_t2[11] <= __startrek_start_t2[12] - 1); assume_abort_if_not(__startrek_end_t2[12] <= __startrek_start_t2[13] - 1); assume_abort_if_not(__startrek_end_t2[13] <= __startrek_start_t2[14] - 1); assume_abort_if_not(__startrek_end_t2[14] <= __startrek_start_t2[15] - 1); assume_abort_if_not(__startrek_end_t2[15] <= __startrek_start_t2[16] - 1); assume_abort_if_not(__startrek_end_t2[16] <= __startrek_start_t2[17] - 1); assume_abort_if_not(__startrek_end_t2[17] <= __startrek_start_t2[18] - 1); assume_abort_if_not(__startrek_end_t2[18] <= __startrek_start_t2[19] - 1); assume_abort_if_not(__startrek_end_t2[19] <= __startrek_start_t2[20] - 1); assume_abort_if_not(__startrek_end_t2[20] <= __startrek_start_t2[21] - 1); assume_abort_if_not(__startrek_end_t2[21] <= __startrek_start_t2[22] - 1); assume_abort_if_not(__startrek_end_t2[22] <= __startrek_start_t2[23] - 1); if (__startrek_start_t0[0] <= __startrek_end_t2[0]) { if (__startrek_start_t2[0] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[0]); assume_abort_if_not(__startrek_end_t2[0] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[0]) { if (__startrek_start_t2[0] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[0]); assume_abort_if_not(__startrek_end_t2[0] < __startrek_end_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[0]) { if (__startrek_start_t2[0] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[0]); assume_abort_if_not(__startrek_end_t2[0] < __startrek_end_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[1]) { if (__startrek_start_t2[1] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[1]); assume_abort_if_not(__startrek_end_t2[1] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[1]) { if (__startrek_start_t2[1] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[1]); assume_abort_if_not(__startrek_end_t2[1] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[0] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[1]) { if (__startrek_start_t2[1] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[1]); assume_abort_if_not(__startrek_end_t2[1] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[0] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[2]) { if (__startrek_start_t2[2] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[2]); assume_abort_if_not(__startrek_end_t2[2] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[2]) { if (__startrek_start_t2[2] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[2]); assume_abort_if_not(__startrek_end_t2[2] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[1] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[2]) { if (__startrek_start_t2[2] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[2]); assume_abort_if_not(__startrek_end_t2[2] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[1] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[3]) { if (__startrek_start_t2[3] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[3]); assume_abort_if_not(__startrek_end_t2[3] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[3]) { if (__startrek_start_t2[3] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[3]); assume_abort_if_not(__startrek_end_t2[3] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[2] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[3]) { if (__startrek_start_t2[3] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[3]); assume_abort_if_not(__startrek_end_t2[3] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[2] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[4]) { if (__startrek_start_t2[4] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[4]); assume_abort_if_not(__startrek_end_t2[4] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[4]) { if (__startrek_start_t2[4] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[4]); assume_abort_if_not(__startrek_end_t2[4] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[3] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[4]) { if (__startrek_start_t2[4] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[4]); assume_abort_if_not(__startrek_end_t2[4] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[3] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[5]) { if (__startrek_start_t2[5] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[5]); assume_abort_if_not(__startrek_end_t2[5] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[5]) { if (__startrek_start_t2[5] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[5]); assume_abort_if_not(__startrek_end_t2[5] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[4] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[5]) { if (__startrek_start_t2[5] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[5]); assume_abort_if_not(__startrek_end_t2[5] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[4] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[6]) { if (__startrek_start_t2[6] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[6]); assume_abort_if_not(__startrek_end_t2[6] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[6]) { if (__startrek_start_t2[6] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[6]); assume_abort_if_not(__startrek_end_t2[6] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[5] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[6]) { if (__startrek_start_t2[6] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[6]); assume_abort_if_not(__startrek_end_t2[6] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[5] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[7]) { if (__startrek_start_t2[7] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[7]); assume_abort_if_not(__startrek_end_t2[7] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[7]) { if (__startrek_start_t2[7] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[7]); assume_abort_if_not(__startrek_end_t2[7] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[6] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[7]) { if (__startrek_start_t2[7] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[7]); assume_abort_if_not(__startrek_end_t2[7] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[6] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[8]) { if (__startrek_start_t2[8] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[8]); assume_abort_if_not(__startrek_end_t2[8] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[8]) { if (__startrek_start_t2[8] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[8]); assume_abort_if_not(__startrek_end_t2[8] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[7] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[8]) { if (__startrek_start_t2[8] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[8]); assume_abort_if_not(__startrek_end_t2[8] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[7] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[9]) { if (__startrek_start_t2[9] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[9]); assume_abort_if_not(__startrek_end_t2[9] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[9]) { if (__startrek_start_t2[9] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[9]); assume_abort_if_not(__startrek_end_t2[9] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[8] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[9]) { if (__startrek_start_t2[9] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[9]); assume_abort_if_not(__startrek_end_t2[9] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[8] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[10]) { if (__startrek_start_t2[10] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[10]); assume_abort_if_not(__startrek_end_t2[10] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[10]) { if (__startrek_start_t2[10] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[10]); assume_abort_if_not(__startrek_end_t2[10] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[9] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[10]) { if (__startrek_start_t2[10] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[10]); assume_abort_if_not(__startrek_end_t2[10] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[9] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[11]) { if (__startrek_start_t2[11] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[11]); assume_abort_if_not(__startrek_end_t2[11] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[11]) { if (__startrek_start_t2[11] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[11]); assume_abort_if_not(__startrek_end_t2[11] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[10] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[11]) { if (__startrek_start_t2[11] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[11]); assume_abort_if_not(__startrek_end_t2[11] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[10] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[12]) { if (__startrek_start_t2[12] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[12]); assume_abort_if_not(__startrek_end_t2[12] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[12]) { if (__startrek_start_t2[12] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[12]); assume_abort_if_not(__startrek_end_t2[12] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[11] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[12]) { if (__startrek_start_t2[12] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[12]); assume_abort_if_not(__startrek_end_t2[12] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[11] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[13]) { if (__startrek_start_t2[13] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[13]); assume_abort_if_not(__startrek_end_t2[13] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[13]) { if (__startrek_start_t2[13] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[13]); assume_abort_if_not(__startrek_end_t2[13] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[12] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[13]) { if (__startrek_start_t2[13] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[13]); assume_abort_if_not(__startrek_end_t2[13] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[12] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[14]) { if (__startrek_start_t2[14] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[14]); assume_abort_if_not(__startrek_end_t2[14] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[14]) { if (__startrek_start_t2[14] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[14]); assume_abort_if_not(__startrek_end_t2[14] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[13] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[14]) { if (__startrek_start_t2[14] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[14]); assume_abort_if_not(__startrek_end_t2[14] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[13] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[15]) { if (__startrek_start_t2[15] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[15]); assume_abort_if_not(__startrek_end_t2[15] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[15]) { if (__startrek_start_t2[15] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[15]); assume_abort_if_not(__startrek_end_t2[15] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[14] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[15]) { if (__startrek_start_t2[15] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[15]); assume_abort_if_not(__startrek_end_t2[15] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[14] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[16]) { if (__startrek_start_t2[16] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[16]); assume_abort_if_not(__startrek_end_t2[16] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[16]) { if (__startrek_start_t2[16] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[16]); assume_abort_if_not(__startrek_end_t2[16] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[15] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[16]) { if (__startrek_start_t2[16] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[16]); assume_abort_if_not(__startrek_end_t2[16] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[15] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[17]) { if (__startrek_start_t2[17] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[17]); assume_abort_if_not(__startrek_end_t2[17] < __startrek_end_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[17]) { if (__startrek_start_t2[17] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[17]); assume_abort_if_not(__startrek_end_t2[17] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[16] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[17]) { if (__startrek_start_t2[17] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[17]); assume_abort_if_not(__startrek_end_t2[17] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[16] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[18]) { if (__startrek_start_t2[18] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[18]); assume_abort_if_not(__startrek_end_t2[18] < __startrek_end_t0[0]); assume_abort_if_not(__startrek_end_t2[0] < __startrek_start_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[18]) { if (__startrek_start_t2[18] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[18]); assume_abort_if_not(__startrek_end_t2[18] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[17] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[18]) { if (__startrek_start_t2[18] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[18]); assume_abort_if_not(__startrek_end_t2[18] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[17] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[19]) { if (__startrek_start_t2[19] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[19]); assume_abort_if_not(__startrek_end_t2[19] < __startrek_end_t0[0]); assume_abort_if_not(__startrek_end_t2[1] < __startrek_start_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[19]) { if (__startrek_start_t2[19] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[19]); assume_abort_if_not(__startrek_end_t2[19] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[18] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[19]) { if (__startrek_start_t2[19] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[19]); assume_abort_if_not(__startrek_end_t2[19] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[18] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[20]) { if (__startrek_start_t2[20] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[20]); assume_abort_if_not(__startrek_end_t2[20] < __startrek_end_t0[0]); assume_abort_if_not(__startrek_end_t2[2] < __startrek_start_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[20]) { if (__startrek_start_t2[20] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[20]); assume_abort_if_not(__startrek_end_t2[20] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[19] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[20]) { if (__startrek_start_t2[20] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[20]); assume_abort_if_not(__startrek_end_t2[20] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[19] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[21]) { if (__startrek_start_t2[21] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[21]); assume_abort_if_not(__startrek_end_t2[21] < __startrek_end_t0[0]); assume_abort_if_not(__startrek_end_t2[3] < __startrek_start_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[21]) { if (__startrek_start_t2[21] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[21]); assume_abort_if_not(__startrek_end_t2[21] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[20] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[21]) { if (__startrek_start_t2[21] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[21]); assume_abort_if_not(__startrek_end_t2[21] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[20] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[22]) { if (__startrek_start_t2[22] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[22]); assume_abort_if_not(__startrek_end_t2[22] < __startrek_end_t0[0]); assume_abort_if_not(__startrek_end_t2[4] < __startrek_start_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[22]) { if (__startrek_start_t2[22] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[22]); assume_abort_if_not(__startrek_end_t2[22] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[21] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[22]) { if (__startrek_start_t2[22] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[22]); assume_abort_if_not(__startrek_end_t2[22] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[21] < __startrek_start_t1[1]); } } } if (__startrek_start_t0[0] <= __startrek_end_t2[23]) { if (__startrek_start_t2[23] <= __startrek_end_t0[0]) { { assume_abort_if_not(__startrek_start_t0[0] <= __startrek_start_t2[23]); assume_abort_if_not(__startrek_end_t2[23] < __startrek_end_t0[0]); assume_abort_if_not(__startrek_end_t2[5] < __startrek_start_t0[0]); } } } if (__startrek_start_t1[0] <= __startrek_end_t2[23]) { if (__startrek_start_t2[23] <= __startrek_end_t1[0]) { { assume_abort_if_not(__startrek_start_t1[0] <= __startrek_start_t2[23]); assume_abort_if_not(__startrek_end_t2[23] < __startrek_end_t1[0]); assume_abort_if_not(__startrek_end_t2[22] < __startrek_start_t1[0]); } } } if (__startrek_start_t1[1] <= __startrek_end_t2[23]) { if (__startrek_start_t2[23] <= __startrek_end_t1[1]) { { assume_abort_if_not(__startrek_start_t1[1] <= __startrek_start_t2[23]); assume_abort_if_not(__startrek_end_t2[23] < __startrek_end_t1[1]); assume_abort_if_not(__startrek_end_t2[22] < __startrek_start_t1[1]); } } } } } __inline void __startrek_init_globals(void) { { _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]; } } __inline static _Bool __startrek_cs_t0(void) { _Bool c1 ; unsigned char o2 ; { if (__startrek_is_first_cs) { { __startrek_is_first_cs = 0; } } if (__startrek_lock) { return (0); } c1 = __VERIFIER_nondet_bool(); if (c1) { return (0); } o2 = __startrek_round; __startrek_round = __VERIFIER_nondet_uchar(); assume_abort_if_not(__startrek_round > o2); assume_abort_if_not(__startrek_round <= __startrek_job_end); if (__startrek_round != __startrek_job_end) { { if (__startrek_start_t1[0] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end_t1[0]); } if (__startrek_start_t1[1] < __startrek_round) { assume_abort_if_not(__startrek_round > __startrek_end_t1[1]); } } } return (1); } } __inline static _Bool __startrek_cs_t1(void) { _Bool c1 ; unsigned char o2 ; { if (__startrek_is_first_cs) { { __startrek_is_first_cs = 0; } } if (__startrek_lock) { return (0); } c1 = __VERIFIER_nondet_bool(); if (c1) { return (0); } o2 = __startrek_round; __startrek_round = __VERIFIER_nondet_uchar(); assume_abort_if_not(__startrek_round > o2); assume_abort_if_not(__startrek_round <= __startrek_job_end); if (__startrek_round != __startrek_job_end) { { } } return (1); } } __inline static _Bool __startrek_cs_t2(void) { { return (0); } } __inline static void __startrek_assert_i0(_Bool arg ) { { if (__startrek_hyper_period != 0) { return; } if (arg) { return; } if (__startrek_round < __startrek_error_round) { __startrek_error_round = __startrek_round; } switch (__startrek_task) { case 0: __startrek_Assert_t0_i0[__startrek_job] = 0; break; case 1: __startrek_Assert_t1_i0[__startrek_job] = 0; break; case 2: __startrek_Assert_t2_i0[__startrek_job] = 0; break; } } } __inline static void __startrek_assert_i1(_Bool arg ) { { if (__startrek_hyper_period != 0) { return; } if (arg) { return; } if (__startrek_round < __startrek_error_round) { __startrek_error_round = __startrek_round; } switch (__startrek_task) { case 0: __startrek_Assert_t0_i1[__startrek_job] = 0; break; case 1: __startrek_Assert_t1_i1[__startrek_job] = 0; break; case 2: __startrek_Assert_t2_i1[__startrek_job] = 0; break; } } } __inline void __startrek_check_assumptions(void) { { assume_abort_if_not(_i_cmd_turn_[26] == _cmd_turn_[25]); assume_abort_if_not(_i_cmd_turn_[25] == _cmd_turn_[24]); assume_abort_if_not(_i_cmd_turn_[24] == _cmd_turn_[23]); assume_abort_if_not(_i_cmd_turn_[23] == _cmd_turn_[22]); assume_abort_if_not(_i_cmd_turn_[22] == _cmd_turn_[21]); assume_abort_if_not(_i_cmd_turn_[21] == _cmd_turn_[20]); assume_abort_if_not(_i_cmd_turn_[20] == _cmd_turn_[19]); assume_abort_if_not(_i_cmd_turn_[19] == _cmd_turn_[18]); assume_abort_if_not(_i_cmd_turn_[18] == _cmd_turn_[17]); assume_abort_if_not(_i_cmd_turn_[17] == _cmd_turn_[16]); assume_abort_if_not(_i_cmd_turn_[16] == _cmd_turn_[15]); assume_abort_if_not(_i_cmd_turn_[15] == _cmd_turn_[14]); assume_abort_if_not(_i_cmd_turn_[14] == _cmd_turn_[13]); assume_abort_if_not(_i_cmd_turn_[13] == _cmd_turn_[12]); assume_abort_if_not(_i_cmd_turn_[12] == _cmd_turn_[11]); assume_abort_if_not(_i_cmd_turn_[11] == _cmd_turn_[10]); assume_abort_if_not(_i_cmd_turn_[10] == _cmd_turn_[9]); assume_abort_if_not(_i_cmd_turn_[9] == _cmd_turn_[8]); assume_abort_if_not(_i_cmd_turn_[8] == _cmd_turn_[7]); assume_abort_if_not(_i_cmd_turn_[7] == _cmd_turn_[6]); assume_abort_if_not(_i_cmd_turn_[6] == _cmd_turn_[5]); assume_abort_if_not(_i_cmd_turn_[5] == _cmd_turn_[4]); assume_abort_if_not(_i_cmd_turn_[4] == _cmd_turn_[3]); assume_abort_if_not(_i_cmd_turn_[3] == _cmd_turn_[2]); assume_abort_if_not(_i_cmd_turn_[2] == _cmd_turn_[1]); assume_abort_if_not(_i_cmd_turn_[1] == _cmd_turn_[0]); assume_abort_if_not(_i_cmd_forward_[26] == _cmd_forward_[25]); assume_abort_if_not(_i_cmd_forward_[25] == _cmd_forward_[24]); assume_abort_if_not(_i_cmd_forward_[24] == _cmd_forward_[23]); assume_abort_if_not(_i_cmd_forward_[23] == _cmd_forward_[22]); assume_abort_if_not(_i_cmd_forward_[22] == _cmd_forward_[21]); assume_abort_if_not(_i_cmd_forward_[21] == _cmd_forward_[20]); assume_abort_if_not(_i_cmd_forward_[20] == _cmd_forward_[19]); assume_abort_if_not(_i_cmd_forward_[19] == _cmd_forward_[18]); assume_abort_if_not(_i_cmd_forward_[18] == _cmd_forward_[17]); assume_abort_if_not(_i_cmd_forward_[17] == _cmd_forward_[16]); assume_abort_if_not(_i_cmd_forward_[16] == _cmd_forward_[15]); assume_abort_if_not(_i_cmd_forward_[15] == _cmd_forward_[14]); assume_abort_if_not(_i_cmd_forward_[14] == _cmd_forward_[13]); assume_abort_if_not(_i_cmd_forward_[13] == _cmd_forward_[12]); assume_abort_if_not(_i_cmd_forward_[12] == _cmd_forward_[11]); assume_abort_if_not(_i_cmd_forward_[11] == _cmd_forward_[10]); assume_abort_if_not(_i_cmd_forward_[10] == _cmd_forward_[9]); assume_abort_if_not(_i_cmd_forward_[9] == _cmd_forward_[8]); assume_abort_if_not(_i_cmd_forward_[8] == _cmd_forward_[7]); assume_abort_if_not(_i_cmd_forward_[7] == _cmd_forward_[6]); assume_abort_if_not(_i_cmd_forward_[6] == _cmd_forward_[5]); assume_abort_if_not(_i_cmd_forward_[5] == _cmd_forward_[4]); assume_abort_if_not(_i_cmd_forward_[4] == _cmd_forward_[3]); assume_abort_if_not(_i_cmd_forward_[3] == _cmd_forward_[2]); assume_abort_if_not(_i_cmd_forward_[2] == _cmd_forward_[1]); assume_abort_if_not(_i_cmd_forward_[1] == _cmd_forward_[0]); assume_abort_if_not(_i_obstacle_flag_[26] == _obstacle_flag_[25]); assume_abort_if_not(_i_obstacle_flag_[25] == _obstacle_flag_[24]); assume_abort_if_not(_i_obstacle_flag_[24] == _obstacle_flag_[23]); assume_abort_if_not(_i_obstacle_flag_[23] == _obstacle_flag_[22]); assume_abort_if_not(_i_obstacle_flag_[22] == _obstacle_flag_[21]); assume_abort_if_not(_i_obstacle_flag_[21] == _obstacle_flag_[20]); assume_abort_if_not(_i_obstacle_flag_[20] == _obstacle_flag_[19]); assume_abort_if_not(_i_obstacle_flag_[19] == _obstacle_flag_[18]); assume_abort_if_not(_i_obstacle_flag_[18] == _obstacle_flag_[17]); assume_abort_if_not(_i_obstacle_flag_[17] == _obstacle_flag_[16]); assume_abort_if_not(_i_obstacle_flag_[16] == _obstacle_flag_[15]); assume_abort_if_not(_i_obstacle_flag_[15] == _obstacle_flag_[14]); assume_abort_if_not(_i_obstacle_flag_[14] == _obstacle_flag_[13]); assume_abort_if_not(_i_obstacle_flag_[13] == _obstacle_flag_[12]); assume_abort_if_not(_i_obstacle_flag_[12] == _obstacle_flag_[11]); assume_abort_if_not(_i_obstacle_flag_[11] == _obstacle_flag_[10]); assume_abort_if_not(_i_obstacle_flag_[10] == _obstacle_flag_[9]); assume_abort_if_not(_i_obstacle_flag_[9] == _obstacle_flag_[8]); assume_abort_if_not(_i_obstacle_flag_[8] == _obstacle_flag_[7]); assume_abort_if_not(_i_obstacle_flag_[7] == _obstacle_flag_[6]); assume_abort_if_not(_i_obstacle_flag_[6] == _obstacle_flag_[5]); assume_abort_if_not(_i_obstacle_flag_[5] == _obstacle_flag_[4]); assume_abort_if_not(_i_obstacle_flag_[4] == _obstacle_flag_[3]); assume_abort_if_not(_i_obstacle_flag_[3] == _obstacle_flag_[2]); assume_abort_if_not(_i_obstacle_flag_[2] == _obstacle_flag_[1]); assume_abort_if_not(_i_obstacle_flag_[1] == _obstacle_flag_[0]); assume_abort_if_not(_i_nxtway_gs_mode_[26] == _nxtway_gs_mode_[25]); assume_abort_if_not(_i_nxtway_gs_mode_[25] == _nxtway_gs_mode_[24]); assume_abort_if_not(_i_nxtway_gs_mode_[24] == _nxtway_gs_mode_[23]); assume_abort_if_not(_i_nxtway_gs_mode_[23] == _nxtway_gs_mode_[22]); assume_abort_if_not(_i_nxtway_gs_mode_[22] == _nxtway_gs_mode_[21]); assume_abort_if_not(_i_nxtway_gs_mode_[21] == _nxtway_gs_mode_[20]); assume_abort_if_not(_i_nxtway_gs_mode_[20] == _nxtway_gs_mode_[19]); assume_abort_if_not(_i_nxtway_gs_mode_[19] == _nxtway_gs_mode_[18]); assume_abort_if_not(_i_nxtway_gs_mode_[18] == _nxtway_gs_mode_[17]); assume_abort_if_not(_i_nxtway_gs_mode_[17] == _nxtway_gs_mode_[16]); assume_abort_if_not(_i_nxtway_gs_mode_[16] == _nxtway_gs_mode_[15]); assume_abort_if_not(_i_nxtway_gs_mode_[15] == _nxtway_gs_mode_[14]); assume_abort_if_not(_i_nxtway_gs_mode_[14] == _nxtway_gs_mode_[13]); assume_abort_if_not(_i_nxtway_gs_mode_[13] == _nxtway_gs_mode_[12]); assume_abort_if_not(_i_nxtway_gs_mode_[12] == _nxtway_gs_mode_[11]); assume_abort_if_not(_i_nxtway_gs_mode_[11] == _nxtway_gs_mode_[10]); assume_abort_if_not(_i_nxtway_gs_mode_[10] == _nxtway_gs_mode_[9]); assume_abort_if_not(_i_nxtway_gs_mode_[9] == _nxtway_gs_mode_[8]); assume_abort_if_not(_i_nxtway_gs_mode_[8] == _nxtway_gs_mode_[7]); assume_abort_if_not(_i_nxtway_gs_mode_[7] == _nxtway_gs_mode_[6]); assume_abort_if_not(_i_nxtway_gs_mode_[6] == _nxtway_gs_mode_[5]); assume_abort_if_not(_i_nxtway_gs_mode_[5] == _nxtway_gs_mode_[4]); assume_abort_if_not(_i_nxtway_gs_mode_[4] == _nxtway_gs_mode_[3]); assume_abort_if_not(_i_nxtway_gs_mode_[3] == _nxtway_gs_mode_[2]); assume_abort_if_not(_i_nxtway_gs_mode_[2] == _nxtway_gs_mode_[1]); assume_abort_if_not(_i_nxtway_gs_mode_[1] == _nxtway_gs_mode_[0]); } } __inline void __startrek_user_init(void) { { } } __inline void __startrek_user_final(void) { { } } __inline void __startrek_check_assertions(void) { { assert(__startrek_Assert_t2_i1[23]); assert(__startrek_Assert_t2_i1[22]); assert(__startrek_Assert_t2_i1[21]); assert(__startrek_Assert_t2_i1[20]); assert(__startrek_Assert_t2_i1[19]); assert(__startrek_Assert_t2_i1[18]); assert(__startrek_Assert_t2_i1[17]); assert(__startrek_Assert_t2_i1[16]); assert(__startrek_Assert_t2_i1[15]); assert(__startrek_Assert_t2_i1[14]); assert(__startrek_Assert_t2_i1[13]); assert(__startrek_Assert_t2_i1[12]); assert(__startrek_Assert_t2_i1[11]); assert(__startrek_Assert_t2_i1[10]); assert(__startrek_Assert_t2_i1[9]); assert(__startrek_Assert_t2_i1[8]); assert(__startrek_Assert_t2_i1[7]); assert(__startrek_Assert_t2_i1[6]); assert(__startrek_Assert_t2_i1[5]); assert(__startrek_Assert_t2_i1[4]); assert(__startrek_Assert_t2_i1[3]); assert(__startrek_Assert_t2_i1[2]); assert(__startrek_Assert_t2_i1[1]); assert(__startrek_Assert_t2_i1[0]); assert(__startrek_Assert_t1_i1[1]); assert(__startrek_Assert_t1_i1[0]); assert(__startrek_Assert_t0_i1[0]); assert(__startrek_Assert_t2_i0[23]); assert(__startrek_Assert_t2_i0[22]); assert(__startrek_Assert_t2_i0[21]); assert(__startrek_Assert_t2_i0[20]); assert(__startrek_Assert_t2_i0[19]); assert(__startrek_Assert_t2_i0[18]); assert(__startrek_Assert_t2_i0[17]); assert(__startrek_Assert_t2_i0[16]); assert(__startrek_Assert_t2_i0[15]); assert(__startrek_Assert_t2_i0[14]); assert(__startrek_Assert_t2_i0[13]); assert(__startrek_Assert_t2_i0[12]); assert(__startrek_Assert_t2_i0[11]); assert(__startrek_Assert_t2_i0[10]); assert(__startrek_Assert_t2_i0[9]); assert(__startrek_Assert_t2_i0[8]); assert(__startrek_Assert_t2_i0[7]); assert(__startrek_Assert_t2_i0[6]); assert(__startrek_Assert_t2_i0[5]); assert(__startrek_Assert_t2_i0[4]); assert(__startrek_Assert_t2_i0[3]); assert(__startrek_Assert_t2_i0[2]); assert(__startrek_Assert_t2_i0[1]); assert(__startrek_Assert_t2_i0[0]); assert(__startrek_Assert_t1_i0[1]); assert(__startrek_Assert_t1_i0[0]); assert(__startrek_Assert_t0_i0[0]); } } void __main(void) { _Bool c1 ; { __startrek_error_round = 27; __startrek_schedule_jobs(); __startrek_init_globals(); { { __startrek_task = 0; __startrek_job = 0; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t0[0]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t0[0]; c1 = __startrek_entry_pt_OSEK_Task_ts3(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } } { __startrek_task = 1; __startrek_job = 0; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t1[0]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t1[0]; c1 = __startrek_entry_pt_OSEK_Task_ts2(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 1; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t1[1]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t1[1]; c1 = __startrek_entry_pt_OSEK_Task_ts2(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } } { __startrek_task = 2; __startrek_job = 0; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[0]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[0]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 1; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[1]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[1]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 2; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[2]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[2]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 3; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[3]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[3]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 4; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[4]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[4]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 5; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[5]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[5]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 6; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[6]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[6]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 7; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[7]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[7]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 8; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[8]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[8]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 9; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[9]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[9]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 10; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[10]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[10]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 11; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[11]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[11]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 12; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[12]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[12]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 13; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[13]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[13]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 14; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[14]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[14]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 15; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[15]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[15]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 16; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[16]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[16]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 17; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[17]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[17]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 18; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[18]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[18]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 19; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[19]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[19]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 20; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[20]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[20]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 21; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[21]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[21]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 22; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[22]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[22]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } __startrek_job = 23; __startrek_is_first_cs = 1; __startrek_round = __startrek_start_t2[23]; if (__startrek_round < __startrek_error_round) { { __startrek_job_end = __startrek_end_t2[23]; c1 = __startrek_entry_pt_OSEK_Task_ts1(); __startrek_lock = 0; assume_abort_if_not(__startrek_round == __startrek_job_end); } } } } __startrek_round = 27; __startrek_check_assumptions(); __startrek_check_assertions(); if (__startrek_hyper_period == 0) { { __startrek_user_final(); } } } } int main(void) { { __startrek_init_shared(); __startrek_user_init(); __startrek_hyper_period = 0; __main(); } return 0; } __inline static unsigned char __startrek_read_nxtway_gs_mode(void) { unsigned char r1 ; _Bool c2 ; unsigned char or3 ; { switch (__startrek_task) { case 0: { or3 = __startrek_round; c2 = __startrek_cs_t0(); { } } break; case 1: { or3 = __startrek_round; c2 = __startrek_cs_t1(); { } } break; case 2: { or3 = __startrek_round; c2 = __startrek_cs_t2(); { } } break; } r1 = _nxtway_gs_mode_[__startrek_round]; return (r1); } } __inline static _Bool __startrek_read_obstacle_flag(void) { _Bool r1 ; _Bool c2 ; unsigned char or3 ; { switch (__startrek_task) { case 0: { or3 = __startrek_round; c2 = __startrek_cs_t0(); { } } break; case 1: { or3 = __startrek_round; c2 = __startrek_cs_t1(); { } } break; case 2: { or3 = __startrek_round; c2 = __startrek_cs_t2(); { } } break; } r1 = _obstacle_flag_[__startrek_round]; return (r1); } } __inline static 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 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 void __startrek_init_shared(void) { { _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; } } void ecrobot_bt_data_logger(char arg0, char arg1) { return; } void ecrobot_sound_tone(unsigned int arg0, unsigned int arg1, char arg2) { return; } void nxt_motor_set_count(unsigned char arg0, char arg1) { return; } void nxt_motor_set_speed(unsigned char arg0, char arg1, char arg2) { return; }