Documentation AK CONTINUOUS - GaloisInc/HighAssuranceControllerOfSelfBalancingRobotCapstone GitHub Wiki

1. Realize I didn't really to modify any of the Ocaml code for this to work.
2. Commented out or deleted all of the Rust code that would prevent embedded from working.
3. Compiled Kind2, compiled the Rust library with kind2, then tested it with arduino. Balancing worked properly.
4. Important note: I have not messed around with assertions yet, so I'm not sure if this will work.
5. I'm not sure what consequences there may be by me using a mutable reference instead of returning a new controller each time like the old generator used to do.
6. Probably a good time to start testing everything and cleaning up for a final handoff.

Currently, my work outside of this repo is split up into these following repos: Artem1199/kind2, Artem1199/otis-arduino, Artem1199/otis-TCP, Artem1199/otis-server. This was done this way because a lot of these projects are forks of other projects or simply don't fit anywhere on this repo.

1. fmt is ocaml format pretty-printer combinator. It exposes Format pretty-print functions.
2. fmt_helpers is a function that acceps fmt and systems
3. 'a -> means the function is taking in multiple "any type" inputs and output
4. -> unit means it is returning a void.

1. First modification to the string printout for helper:: function resulted in a compile error with Ocaml

• Type 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j is not compatible with type unit

2. Somehow I modified the string and changed it's type.
3. I think I have an easy way around this. Comment out the code I don't need instead of deleting it. Should save some time on having to edit all these strings. Avoid dealing with Ocaml as much as possible.

1. Ocaml function calls are different In general the rule is: "bracket around the whole function call — don't put brackets around the arguments to a function call"
2. This is how you define a function let average a b = (a +. b) /. 2.0;;
3. Essentially avoid parenthesis. The function starts after the =.
4. OCaml doesn't have a return keyword — the last expression in a function becomes the result of the function automatically.

1. Modifying the Lustre generator file. This modification will occur on my fork on Kind2: lustreToRust
2. A nice feature would be to add a way call either the embedded Rust compile or the normal stdin compilation.
   1. Could implement this in Flags.ml. Then modify postAnalysis.ml deal with the flag. Stretch goal if time allows.
3. Noticed 1 restriction is that my output if a f64. This could be a problem if we want something besides f64 output. Or if we have multiple outputs.
   1. Found very easy solution to this. Simply use the already created Output function to return Self::Output type!
4. Cheatsheet from last modification:

• 1. Modify input_of to accept (array: Self::Array) instead of vec<String> -done
• 2. Modify read_input and read_next
• 3. Replace Result<Self::Input, String> with Self::Input (Ditto for Self::Output equivalents)
• 4. Remove fn output_str, this outputs a string for command-line examples, don't need this.
• 5. Create fn output_flt, this is necessary to return our Real value for use by C++
• 5. Remove fn run, this creates a loop, we don't need this since Arduino/C++ will provide the looping
• 7. Remove or replace all /// documentation
• 8. Remove clamp_and_run
• 9. Remove parse, this uses std library that we want to avoid
• 10. Remove InputReader, uses std
• 11. Remove help() and error <>, uses std

5. I found a way to compile the kind2 program with my modifications. Running:

ocamlbuild -j 0 -pkg yojson -cflags -w,@P@U@F kind2.native

Inside the kind2/src folder will build kind2 without building the other OCaml components. Problem is now I have to learn how to program Ocaml

1. Can't seem to call the read_next function outside of the trait.
2. The issue is that I want to input a mutable reference, but an I can't because everything inside the trait and all the implementations is not mutable.
3. Considered modifying everything to have a mutable reference for FFI, and ignore it with the embedded compiler.
4. Creating InputReader, creates a type that reads from the input cmd line input stream.
5. The program waits for Enter to be pressed at read_line.
6. Making this FFI compatible is a nightmare..
   1. We have to pass in a mutable reference to the memory location, but lus generated code does not work that way.
   2. Attempt to return all new states that are returned with .next. This was it just modifies the 1 struct instead of overriding the old struct each time.
   3. Having a hard time understanding the mutable reference, here's a definition `Using the mutable reference means you're referencing the place in memory where the variable x is stored. Across function boundaries, you're able to change the value stored in memory there.
   4. Removed the -> Self on all next functions. This way nothing is returned. Only the struct is modified, means we don't have to copy anything. Got the library to compile and ran it on the arduino.
   5. Noticed I wrote the original lustre program PID wrong and have to fix it in Rust code. This is mostly to test functionality, not for compiler modification.
7. Fixing Lustre generated PID:'
   1. I believe I only really have to modify my 1 comptue_calc function.
   2. Corrected the 1 function, and had to correct array inputs because arrays also needs Rust/C++ FFI.
   3. Outputs of old PID and this new lustre generated PID are equal.
8. Robot is balancing itself with the modified lustre PID!!
9. Next step modifying Lustre generator.

Try removing the return on Self.

1. Issues with Self when used as input, error for expected one of 9 possible tokens, while Self:: on output works fine.
2. A lot of programmers use Rust generics instead of types for traits in embedded Rust.
3. Generics allow users to share the same function for multiple types.
4. Found an example of Self used in a trait, and replaced my Self::Array with array: Self::Array, this seemed to compile. Not sure why this difference occurs in the no_std version.
5. Having an issue with using the trait function read_init outside of the trait.

1. New robot can self balance with Rust PID.
   1. Removed the additional YAW pid to simplify things for now. May need to reintroduce in the future.
   2. There is an issue with setpoint slightly changing after not using the robot for a while. Not sure how to deal with that atm.
   3. Some references; Great video for PID calibration, Another video on uses for the encoders + kalman filter, also consider impacts of battery drain.

1. Modify the init method construct to create a Compute based on direct inputs instead of the Input type.
   1. Will have to return Self instead of Result
   2. Remove all Ok returns and try! statements
2. Limit function returns two results, then Input and the Output
3. Have to modify the declarations in Sys as well
   1. The issue with removing Input types, is that Input varies depending on the structure.
4. Branching off the previous issue, it would be preferable to keep Input the same, instead, we modify input_of to create out Input type.
   1. Input_of uses std::parse to convert our input string to a Real, we are not going to feed string values, so we don't have a need for parse.
   2. Input_of gets fed a vec from read_inputs that converts our command line input string to a vec
   3. The whole program is structured to have the trait of Sys, which is the same for every function and node.
   4. This creates an issue because we want a uniquely sized input for every single function. We also can't really use a Vec input because C++ needs a specific size to allocate memory for.
   5. If we assume the parent function will have the largest number of inputs, then we can have the Sys use an array as large as the largest input. I don't believe that assumption is always true, internal functions could take something like constants that would not be input in the parent function.
   6. In C++ we would also have to allocate memory for every node or function's struct. Whenever I call a method of a struct I have to also supply the reference to the struct. This is pretty standard for most of the Rust functions generated by Kind2, so no need to worry.
   7. We want to have a set size if we want this to work with C++. We can use vec with the collections crate, and a global allocator, but that doesn't seem reliable. I don't believe Rust is allowed to allocate memory when Arduino is the main program.
   8. One alternative is to introduce shim functions outside of the Kind2 compiler that is meant to interface with C++.
      1. This way C++ allocates memory for a vec, then have Rust populate that vector and feeds it into a function that calls input_of. Example of C++, Rust vector gibberish.
5. I don't think there is a way of doing this, and keeping Sys trait the same everywhere. What if we had an array of size arity()
   1. The input array size can be a value of the struct itself! Meaning we can keep Sys intact! :D
6. Order of run is: InputReader -> read_init -> Self::input_of -> Self::init -> loop (read_next -> Self::input_of)

1. Modify input_of to accept [Real; svar_arraySize: usize] instead of vec<String>
2. Modify read_input and read_next
3. Replace Result<Self::Input, String> with Self::Input (Ditto for Self::Output equivalents)
4. Remove fn output_str, this outputs a string for command-line examples, don't need this.
5. Create fn output_flt, this is necessary to return our Real value for use by C++
6. Remove fn run, this creates a loop, we don't need this since Arduino/C++ will provide the looping
7. Remove or replace all /// documentation
8. Remove clamp_and_run
9. Remove parse, this uses std library that we want to avoid
10. Remove InputReader, uses std
11. Remove help() and error <>, uses std

9. Replace Input type with Array type, and remove input_of

1. Will need to add shim functions for read_init and read_next
   1. Is it possible to make this a trait?

1. The robot is working pretty well, but now I have to figure out a way to get the PID to interact with the motors properly.

1. Worked on mounting MKR1010 board and MPU6050 board ontop of robot. Mostly wiring.
2. Hotglue isn't good enough to hold the robot. Robot fell apart when trying to move batteries. Hotglued again for now.
3. Adafruit motor shield required 4 connections, SCL, SDA, 5V, and GND. (For some reason it won't work w/o the 5v). The default I2C address is 0x60.

1. Will have to focus on completing robot and work in Lustre->Rust conversion later.

1. So I want to hijack init to create the Compute struct and initialize it, then return the struct.
   1. I don't care about a result, because Arduino does can't do anything with it.
2. Use (1.0,2.0,...,7.0) to create an equivalent Input type.

1. Rust Result is a richer version of options, which has 2 options either Ok(T), an element T was found, or Err(E), an error was found.
   1. Enums, Options: Options are either Some or None. This can be dealt with match for example
   2. Some(c) => c.to_string(), //if something found, then convert c to string
   3. None => "Error not found".to_string() //Don't find it, then have an alternative response.
2. So returning Result<Self, String> returns either the struct itself if everything is OK or an error string with an error message if there was a failure. Similar to LabVIEW passing through an error. With the result you have to use a match to distinguish between the Ok or the Err.
3. try! Helper macro for unwrapping Result values, will return Err if error occurs in the function call.

1. Need a way to run two separate libraries at once under 1 testbench. Each library has its own TOML file and in/out method. Lus generated PID breakdown
2. main runs clap_and_run()
3. clap_and_run() checks for command line args like --help or --limit, etc. to run individual functions.
4. limit seems to be working exactly as expected.
   1. Anything above 1k is set to 1k, anything below -1k is set to -1k
5. run() method of each function:
   1. Runs InputReader::mk() create an InputReader
   2. Runs read_init using the reader mut and checks for errors
   3. Then invokes read_next on a loop
6. InputReader: creates a buffer with_capacity(100), and a stdin() input.
7. read_input(): InputReader data, separates out the values in the commas, checks for "exit" or "quit", places values in a vec, returns the vec
8. read_init(): runs read_input to get vec, then runs ::init on the inputs to get initial state
9. read_next(): runs self.next on inputs to get next state.
10. self::init: Creates structure with initial values, computes initial states, returns the initial state.
11. self.next: Takes input values, computes next state
12. Trait Sized, a trait that all systems must implement, including Input, Output, input_of, init, next, read_init, read next, etc..
13. Compute() requires an Input type input, Input type is created using input_of
14. impl, implement are trait called Sys, which has various types and functions.
    1. pub trait simply gives a basic overview of the functions and types
    2. impl Sys for xxxxxx describes details specific to each class.

1. Create
2. Run self::init to initialize PID and run 1st calculation.
3. Run self.next each time a view value needs to be computed.
4. Compute init will call Compute_calc init.
5. Preferrable we modify init and next to be used without a Self::Input input, but with a function input.

1. cargo build --bins to build binaries, ./target/debug/Compute_implem to run the binary, use --XXXX to run specific function.
2. Compute() runs Compute_calc to account for time Sampling intervals
3. limit() limits the output between -1k to 1k
4. Need to implement wrap-to-pi in lustre

1. Update submodules to include TCP, Webserver, and Arduino
2. Continue finding way to run lus generated PID w/o stdin stdout transactions.

1. Using OPAM makes this process much easier.
2. Ran into the following error: fatal: No names found, cannot describe anything. This seems like an issue related to git. Forked my own copy of Kind2, and fixed my --prefix= seemed to resolve the issue.

1. Need to create a rust testbench for comparing the Lustre generated PID with the PID written in Rust.
2. Rust has a few ways to write tests, first, the library is recommended to be initialized with: cargo new NAME --lib
3. Had an issue with try! causing rust compile fails. Removed edition = "2018" from the toml file resolved this.