CopilotSing.c

#include <stdbool.h>
#include <stdint.h>


#include "WProgram.h"

int32_t notes[47] = {1519,1519,1519,1519,1519,1519,1519,1275,1915,1700,1519,1432,1432,1432,1432,1432,1519,1519,1519,1700,1700,1519,1700,1275,1519,1519,1519,1519,1519,1519,1519,1275,1915,1700,1519,1432,1432,1432,1432,1432,1519,1519,1275,1275,1432,1700,1915};
int32_t beats[47] = {1,1,2,1,1,2,1,1,1,1,4,1,1,1,1,1,1,2,1,1,1,1,2,2,1,1,2,1,1,2,1,1,1,1,4,1,1,1,1,1,1,2,1,1,1,1,4};
void playtone(int32_t , int32_t , int32_t);


static uint64_t __global_clock = 0;



struct {  /* copilotStateCopilotSing */
  struct {  /* CopilotSing */
    int32_t prophVal__idx[2];
    bool playNote;
    int32_t odd;
    int32_t notes;
    int32_t idx;
    int32_t even;
    int32_t duration;
    uint64_t updateIndex__idx;
    uint64_t outputIndex__idx;
    int32_t tmpSampleVal__notes_Varidx;
    int32_t tmpSampleVal__beats_Varidx;
  } CopilotSing;
} copilotStateCopilotSing =
{  /* copilotStateCopilotSing */
  {  /* CopilotSing */
    /* prophVal__idx */
    { 0L
    , 0L
    },
    /* playNote */  false,
    /* odd */  0L,
    /* notes */  0L,
    /* idx */  0L,
    /* even */  0L,
    /* duration */  0L,
    /* updateIndex__idx */  1ULL,
    /* outputIndex__idx */  0ULL,
    /* tmpSampleVal__notes_Varidx */  0L,
    /* tmpSampleVal__beats_Varidx */  0L
  }
};

/* CopilotSing.updateOutput__playNote */
static void __r0() {
  bool __0 = true;
  if (__0) {
  }
  copilotStateCopilotSing.CopilotSing.playNote = __0;
}

/* CopilotSing.updateOutput__odd */
static void __r1() {
  bool __0 = true;
  uint64_t __1 = 0ULL;
  uint64_t __2 = copilotStateCopilotSing.CopilotSing.outputIndex__idx;
  uint64_t __3 = __1 + __2;
  uint64_t __4 = 2ULL;
  uint64_t __5 = __3 % __4;
  int32_t __6 = copilotStateCopilotSing.CopilotSing.prophVal__idx[__5];
  int32_t __7 = 2L;
  int32_t __8 = __6 % __7;
  int32_t __9 = 1L;
  bool __10 = __8 == __9;
  int32_t __11 = 11L;
  int32_t __12 = 12L;
  int32_t __13 = __10 ? __11 : __12;
  if (__0) {
  }
  copilotStateCopilotSing.CopilotSing.odd = __13;
}

/* CopilotSing.updateOutput__notes */
static void __r2() {
  bool __0 = true;
  int32_t __1 = copilotStateCopilotSing.CopilotSing.tmpSampleVal__notes_Varidx;
  if (__0) {
  }
  copilotStateCopilotSing.CopilotSing.notes = __1;
}

/* CopilotSing.update__idx */
static void __r3() {
  bool __0 = true;
  uint64_t __1 = 0ULL;
  uint64_t __2 = copilotStateCopilotSing.CopilotSing.outputIndex__idx;
  uint64_t __3 = __1 + __2;
  uint64_t __4 = 2ULL;
  uint64_t __5 = __3 % __4;
  int32_t __6 = copilotStateCopilotSing.CopilotSing.prophVal__idx[__5];
  int32_t __7 = 1L;
  int32_t __8 = __6 + __7;
  uint64_t __9 = copilotStateCopilotSing.CopilotSing.updateIndex__idx;
  if (__0) {
  }
  copilotStateCopilotSing.CopilotSing.prophVal__idx[__9] = __8;
}

/* CopilotSing.updateOutput__even */
static void __r6() {
  bool __0 = true;
  uint64_t __1 = 0ULL;
  uint64_t __2 = copilotStateCopilotSing.CopilotSing.outputIndex__idx;
  uint64_t __3 = __1 + __2;
  uint64_t __4 = 2ULL;
  uint64_t __5 = __3 % __4;
  int32_t __6 = copilotStateCopilotSing.CopilotSing.prophVal__idx[__5];
  int32_t __7 = 2L;
  int32_t __8 = __6 % __7;
  int32_t __9 = 1L;
  bool __10 = __8 == __9;
  int32_t __11 = 12L;
  int32_t __12 = 11L;
  int32_t __13 = __10 ? __11 : __12;
  if (__0) {
  }
  copilotStateCopilotSing.CopilotSing.even = __13;
}

/* CopilotSing.updateOutput__duration */
static void __r7() {
  bool __0 = true;
  int32_t __1 = copilotStateCopilotSing.CopilotSing.tmpSampleVal__beats_Varidx;
  int32_t __2 = 300L;
  int32_t __3 = __1 * __2;
  if (__0) {
  }
  copilotStateCopilotSing.CopilotSing.duration = __3;
}

/* CopilotSing.output__idx */
static void __r4() {
  bool __0 = true;
  uint64_t __1 = copilotStateCopilotSing.CopilotSing.outputIndex__idx;
  uint64_t __2 = 1ULL;
  uint64_t __3 = __1 + __2;
  uint64_t __4 = 2ULL;
  uint64_t __5 = __3 % __4;
  int32_t __6 = copilotStateCopilotSing.CopilotSing.prophVal__idx[__1];
  if (__0) {
  }
  copilotStateCopilotSing.CopilotSing.outputIndex__idx = __5;
  copilotStateCopilotSing.CopilotSing.idx = __6;
}

/* CopilotSing.trigger_playNote_playtone___const_13_notesduration_ */
static void __r8() {
  bool __0 = copilotStateCopilotSing.CopilotSing.playNote;
  if (__0) {
    playtone(13 , copilotStateCopilotSing.CopilotSing.notes , copilotStateCopilotSing.CopilotSing.duration);
  }
}

/* CopilotSing.trigger_playNote_digitalWrite__odd_const_1__ */
static void __r9() {
  bool __0 = copilotStateCopilotSing.CopilotSing.playNote;
  if (__0) {
    digitalWrite(copilotStateCopilotSing.CopilotSing.odd , 1);
  }
}

/* CopilotSing.trigger_playNote_digitalWrite__even_const_0__ */
static void __r10() {
  bool __0 = copilotStateCopilotSing.CopilotSing.playNote;
  if (__0) {
    digitalWrite(copilotStateCopilotSing.CopilotSing.even , 0);
  }
}

/* CopilotSing.sample__beats_Varidx */
static void __r11() {
  bool __0 = true;
  int32_t __1 = copilotStateCopilotSing.CopilotSing.idx;
  int32_t __2 = beats[__1];
  if (__0) {
  }
  copilotStateCopilotSing.CopilotSing.tmpSampleVal__beats_Varidx = __2;
}

/* CopilotSing.sample__notes_Varidx */
static void __r12() {
  bool __0 = true;
  int32_t __1 = copilotStateCopilotSing.CopilotSing.idx;
  int32_t __2 = notes[__1];
  if (__0) {
  }
  copilotStateCopilotSing.CopilotSing.tmpSampleVal__notes_Varidx = __2;
}

/* CopilotSing.incrUpdateIndex__idx */
static void __r5() {
  bool __0 = true;
  uint64_t __1 = copilotStateCopilotSing.CopilotSing.updateIndex__idx;
  uint64_t __2 = 1ULL;
  uint64_t __3 = __1 + __2;
  uint64_t __4 = 2ULL;
  uint64_t __5 = __3 % __4;
  if (__0) {
  }
  copilotStateCopilotSing.CopilotSing.updateIndex__idx = __5;
}



void CopilotSing() {
  {
    static uint8_t __scheduling_clock = 0;
    if (__scheduling_clock == 0) {
      __r0();  /* CopilotSing.updateOutput__playNote */
      __r1();  /* CopilotSing.updateOutput__odd */
      __r2();  /* CopilotSing.updateOutput__notes */
      __r3();  /* CopilotSing.update__idx */
      __r6();  /* CopilotSing.updateOutput__even */
      __r7();  /* CopilotSing.updateOutput__duration */
      __scheduling_clock = 3;
    }
    else {
      __scheduling_clock = __scheduling_clock - 1;
    }
  }
  {
    static uint8_t __scheduling_clock = 1;
    if (__scheduling_clock == 0) {
      __r4();  /* CopilotSing.output__idx */
      __scheduling_clock = 3;
    }
    else {
      __scheduling_clock = __scheduling_clock - 1;
    }
  }
  {
    static uint8_t __scheduling_clock = 2;
    if (__scheduling_clock == 0) {
      __r8();  /* CopilotSing.trigger_playNote_playtone___const_13_notesduration_ */
      __r9();  /* CopilotSing.trigger_playNote_digitalWrite__odd_const_1__ */
      __r10();  /* CopilotSing.trigger_playNote_digitalWrite__even_const_0__ */
      __r11();  /* CopilotSing.sample__beats_Varidx */
      __r12();  /* CopilotSing.sample__notes_Varidx */
      __scheduling_clock = 3;
    }
    else {
      __scheduling_clock = __scheduling_clock - 1;
    }
  }
  {
    static uint8_t __scheduling_clock = 3;
    if (__scheduling_clock == 0) {
      __r5();  /* CopilotSing.incrUpdateIndex__idx */
      __scheduling_clock = 3;
    }
    else {
      __scheduling_clock = __scheduling_clock - 1;
    }
  }

  __global_clock = __global_clock + 1;

}

void playtone(int32_t speaker , int32_t tone , int32_t duration){
#ifdef CBMC
  for (int32_t i = 0; i < 1; i ++) {
#else
  for (int32_t i = 0; i < duration * 1000; i += tone * 2) {
#endif
    digitalWrite(speaker, HIGH);
    delayMicroseconds(tone);
    digitalWrite(speaker, LOW);
    delayMicroseconds(tone);
  }
}

void setup(){
   pinMode(13 , OUTPUT);
   pinMode(12 , OUTPUT);
   pinMode(11 , OUTPUT);
}

void loop(){
    CopilotSing();
    delay(3);
}

//Just for calling CBMC.
void cbmc(){
  setup();
  while(1) {
    CopilotSing();
    delay(3);
  }
}