MiPal

Machine Intelligence and Pattern Analysis Laboratory

Downloads

MiEditLLFSM (Java editor of logic labelled finite states machines for clfsm)

  1. MiEditLLFSM.jar.gz: The executable (needs java v7).
  2. HowToUse.pdf : The PDF guide on how to use MiEditLLFSM
  3. EPuckLineFollower: : The clfsm machine used in the example of a finite-state machine that controls an e-Puck in Webots to follow a line (this needs clfsm, and the MiPal Whiteboard gusimplewhiteboard, the guwebotsbridge)
  4. MiEditV2: Version 2 is a prototype to edit Meta-Model LLFSMs in an independent java application (outside Eclipse)
  5. JavaLLFSMsTransformationV1: Prototype of Model-To-Text transformations as a pure java application (no ATL and outside Eclipse, but EMF-based)

MiPal clfsm (and basic tools) for ROS-2-colcon

(recommended Ubuntu 24.04 and Ros-Humble; others are possible but you are required to use clang compatible with c++11)
  1. plain_clfsm_ws.tar.gzThe colcon ROS-2 workspace with sources of clfsm, its library libclfsm, without the MiPal whiteboard (gusimplewhiteboard).
  2. How To Use clfsm with ROS-2 (a PDF document) with 3 logic-labeled finite-state machine examples
    1. The code(clfsmRos2DemoMachines.tar.gz) for the four llfsms used as examples (we recommend you use MiEditLLFSM) but you can use this this code following the instructions above (it also includes the script machine_colcon_setup.sh to setup for compilation with colcon by building the CMakeLists.txt for each package.
    2. The code (turtle_sensor_poster_ws.tar.gz) of a wrapper on the pose of ROS turtlesim for the third machine.
    3. The video MiEditLLFSM used in building a demo llfsm for clfsm to run in ROS 2 and the video Running three demo llfsms with clfsm in ROS 2 demonstrate step by step running demo machines.

MiPal clfsm (and basic tools) for ROS-1-catkin

(recommended Ubuntu 14.04 and Ros-Indigo, recommended MacOS Mavericks and Ros-Hydro; others are possible but you are required to use clang compatible with c++11)
  1. clfsm.tar.bz2 The catkin workspace with sources of clfsm, its library libclfsm, if the MiPal whiteboard is desirable gusimplewhiteboard.
  2. How To Use clfsm with ROS( a PDF document) with 3 logic-labeled finite-state machine examples (script to make catkin packages from the examples machine_catkin_setup.sh). A video demonstrating these ROS packages and how to run the three example LLFSMs is https://www.youtube.com/watch?v=iUNjrS9P9A4&feature=youtu.be
    1. The code(clfsmRosDemoMachines.tar.gz) for the three llfsms used as examples (but really, we recommend you use MiEditLLFSM) before you look at this code.
    2. A ROS package (turtle_sensor_poster.tar.gz) that implements the ROS::service used in the 3rd example machine.
    3. Videos of these machines can be seen at
  3. How To Use gusimplewhiteboard with ROS( a PDF document) with 3 logic-labeled finite-state machine examples
    1. The generator (guwhiteboardtypegenerator.tar.gz )of gusimplewhiteboard types.
    2. The catkin package webots_epuck_nxt_differential_robot (webots_epuck_nxt_differential_robot.tar.gz)and examples used in the "How to Use"
    3. The first machine used in the "How To Use" (ePuckBehavior.tar.gz).
    4. The second machine used in the "How To Use" (FollowLine.tar.gz).
    5. The Makefile for these machines
  4. The C++ driver and the ROS-controller for LEGO NXT. This allows you to build programs for the brick.
    1. The plain NXT_driver is now provided at github
      1. git clone https://github.com/mipalgu/NXTdriver.git
    2. The ROS_NXT controller allows to command the LEGO_NXT when built as a differential robots with motors in ports B and C is now also provided at github
      1. git clone https://github.com/mipalgu/NXTcontroller.git
    3. The documentation that combines the NXTdriver, the controller and clfsm is HowToUseNXTdriver.pdf
      1. The example of an llfsm (motorTest.machine.tar.gz)using the robot LegoNXT. The machine (motorTest.machine.tar.gz) and its Makefile.

Docker containers for model-2-model transformations using the software JavaLLFSMsTransformation and its associated tools.

JavaLLFSMsTransformation enables the construction of executable models of behaviour (as logic-labelled finite-state machines) that can be transformed either into executable models (in C, MIPS, or LISP) or into formal models (in NuSMV or TLA+) for formal verification.
  1. ``How To'' document (HowToUseM2T.pdf) to use the container
  2. The containers in docker hub.

ATL-code for the prototype model-2-model transformations

  1. Algorithms described in Carrillo, M., Estivill-Castro, V. and Rosenblueth, D. ``Model-to-Model Transformations for Efficient Time-domain Verification of Concurrent Models by NuSMV Modules.'' In Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2020) , pages 287-298 ISBN: 978-989-758-400-8.
    1. ATL-transformations.tar The package with some examples and LISP interpreter for LLFSMs in XMI format
    2. YouTube Video demonstrating the prototype ATL transformations.
    3. YouTube Video demonstrating the prototype of a GUI that emulates a trace from the model checker.
  2. Improved implementation ATL-TransformationsV2andNuSMVEmulator.tar.gz including the java emulator and ATL-transformation to remove sections in states. as per the extended paper Carrillo, M., Estivill-Castro, V. and Rosenblueth, D. ``Verification and Simulation of Time-Domain Properties for Models of Behaviour.'' Selected papers from the 8th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2020) , Springer-Verlag