April 7 Documentation AK (Lustre Library to Rust) - GaloisInc/HighAssuranceControllerOfSelfBalancingRobotCapstone GitHub Wiki

  1. Creating Lustre PID library to use in Rust
    1. Wrote a library that can be compiled in Kind2, but fails to compile in Rust: Some equations use undefined variables
    2. Both variables are related to the function I am using. Rewrite Lustre code using node instead of function, same issue.
    3. Tried replacing hardcoded 1000.0 values with inputs/outputs didn't work.
    4. Replacing function with inline code resolved the issue.
    5. Strange issue; if I comment out the limit function, then the inline code doesn't work. Issue with compiler?
    6. Cargo build still works despite the issue.
  2. Comparing Lustre Generated PID vs. Rust PID