lazy_sa_commented.sa 3.8 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109
  1. module Lazy_SA
  2. /*
  3. * The purpose of this adaptation is to only run the internal FMU
  4. * when any of its inputs changes, or when it requests to be explicitly run.
  5. */
  6. semantic adaptation reactive moore LazySA lazy_sa
  7. at "./path/to/LazySA.fmu"
  8. for inner fmu Controller controller
  9. at "./path/to/Controller.fmu"
  10. with input ports obj_detected, passenger_up, passenger_down, passenger_stop, driver_up, driver_down, driver_stop
  11. with output ports up, down, stop
  12. /*
  13. * In addition, we do not need to do anything about the outputs of the inner FMU, because they are zero order holded by default.
  14. */
  15. input ports obj_detected -> controller.obj_detected,
  16. passenger_up -> controller.passenger_up,
  17. passenger_down -> controller.passenger_down,
  18. passenger_stop -> controller.passenger_stop,
  19. driver_up -> controller.driver_up,
  20. driver_down -> controller.driver_down,
  21. driver_stop -> controller.driver_stop
  22. output ports up, down, stop
  23. param INIT_OBJ_DETECTED := false,
  24. INIT_PASSENGER_UP := false,
  25. INIT_PASSENGER_DOWN := false,
  26. INIT_PASSENGER_STOP := false,
  27. INIT_DRIVER_UP := false,
  28. INIT_DRIVER_DOWN := false,
  29. INIT_DRIVER_STOP := false;
  30. control var tn := -1.0,
  31. tl := -1.0,
  32. prev_obj_detected := INIT_OBJ_DETECTED,
  33. prev_passenger_up := INIT_PASSENGER_UP,
  34. prev_passenger_down := INIT_PASSENGER_DOWN,
  35. prev_passenger_stop := INIT_PASSENGER_STOP,
  36. prev_driver_up := INIT_DRIVER_UP,
  37. prev_driver_down := INIT_DRIVER_DOWN,
  38. prev_driver_stop := INIT_DRIVER_STOP;
  39. control rules {
  40. // This initialisation covers simulations that start at a non-zero time.
  41. if (tl < 0.0){
  42. tl := t;
  43. }
  44. var step_size := min(H, tn - t); // In case tn < t, this ensures that the controller will be run at the right time.
  45. // Note that the expression lazy_sa.obj_detected gets replaced by the corresponding storage var in the canonical version.
  46. if (lazy_sa.obj_detected != prev_obj_detected or
  47. lazy_sa.passenger_up != prev_passenger_up or
  48. lazy_sa.passenger_down != prev_passenger_down or
  49. lazy_sa.passenger_stop != prev_passenger_stop or
  50. lazy_sa.driver_up != prev_driver_up or
  51. lazy_sa.driver_down != prev_driver_down or
  52. lazy_sa.driver_stop != prev_driver_stop or
  53. (t+H) >= tn
  54. ){
  55. var step_to_be_done := (t+H-tl);
  56. var step_done := do_step(controller, t, step_to_be_done); // calls the mapIn function that will take care of forwarding the values of the input ports to the internal FMU.
  57. // We calculate these as if step_done == step_to_be_done. If that is not the case, a rollback will be done anyway.
  58. tn := tl + step_done + get_next_time_step(controller); // calculates the next time step that is tolerated by the controller.
  59. /*
  60. The get_next_time_step(controller) function is equivalent to the following snippet:
  61. save_state(controller);
  62. internal_transition := do_step(controller, last_execution_time(controller), MAX);
  63. next_time_step := last_execution_time(controller) + internal_transition;
  64. rollback(controller);
  65. */
  66. // This is the actual step size taken, from the outside world:
  67. step_size := tl + step_done - t; // assert step_size <= H
  68. tl := tl + step_done; // assert tl == t+H
  69. }
  70. // Store the previous values of the inputs
  71. prev_obj_detected := lazy_sa.obj_detected;
  72. prev_passenger_up := lazy_sa.passenger_up;
  73. prev_passenger_down := lazy_sa.passenger_down;
  74. prev_passenger_stop := lazy_sa.passenger_stop;
  75. prev_driver_up := lazy_sa.driver_up;
  76. prev_driver_down := lazy_sa.driver_down;
  77. prev_driver_stop := lazy_sa.driver_stop;
  78. return step_size;
  79. }
  80. /*
  81. The following code is not needed because the outputs are zero order hold'ed by default:
  82. out var stored_up := INIT_UP,
  83. stored_down := INIT_DOWN,
  84. stored_stop := INIT_STOP;
  85. out rules{
  86. true -> {
  87. stored_up := controller.up;
  88. stored_down := controller.down;
  89. stored_stop := controller.stop;
  90. } --> {
  91. lazy_sa.up := stored_up;
  92. lazy_sa.down := stored_down;
  93. lazy_sa.stop := stored_stop;
  94. };
  95. }
  96. */