Project

General

Profile

History

ProSkill

ProSkill is a Procedural Skill langage to program execution/acting component for autonomous robots. This Paper describes most features of the ProSkill langage. Yet, its main interest is that the programs written in this langage can automatically be translated in an equivalent Fiacre formal model, which can then be used with the Tina toolbox (to prove some formal properties using model checking), but also with the Hippo engine to execute the equivalent formal model of the program.

LICENCE

Copyright (c) 2023-2024 Francois Felix Ingrand and LAAS/CNRS All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

  • Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

  • Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

WEBSite

https://redmine.laas.fr/projects/proskill

Documentation

https://redmine.laas.fr/projects/proskill/pages/README.adoc

Installation

PREREQUISITES

We use autotools, all prerequisites should be taken care of…​ just install whatever configure instruct you too.

SUPPORTED PLATFORMS

Any linux/unix…​

You need to install Tina and Fiacre/Hippo, and set the following environment variables:

export HIPPO_DIST=/home/felix/work/hippo-2.7.1
export TINA_DIST=/home/felix/work/tina-3.7.5

to the proper values.

Note The Hippo distribution is in fact a frac distribution to which the hippo engine is added.

INSTALLATION INSTRUCTIONS

git://redmine.laas.fr/laas/users/felix/proskill.git
cd proskill
./bootstrap.sh

After the bootstrap:

./configure
make install

OR you may build proskill in a specific directory:

mkdir build
cd build
../configure
make install

Note that if you do not intend to install ProSkill in the standard /usr/local directory you may have to specify the --prefix=<dir> Similarly, if you plan to have more than one architecture-dependent file in the same tree you may want to specify the --exec-prefix=<bindir>

In any case, the bin directory of the targeted prefix should be in you PATH environment variable.

EXAMPLES

The subdirectory examples contains a number of…​ examples and a Makefile to run them. Most example are for offline verification. Check the Makefile to tweak which model you want to synthesize and check.

The subdirectory examples/drone-hippo contains some C code (with bootstrap.sh, configure.ac, Makefile.am) to setup an online verification with Hippo. One need to install the drone genom3 components as well as the gazebo plugins to run it though.

https://git.openrobots.org/projects/telekyb3/pages/software/run/quadrotor-simulation

You will also need the maneuver-genom3 component to be installed.

Change the shell script and add maneuver in the list of components to start:

components="
  rotorcraft
  nhfc
  pom
  optitrack
  maneuver
"

Change the tcl script to load the maneuver conponent and set it up.

Here are the commands you will need to add to the tcl scripts, after the commented lines

# load components clients
$g load maneuver

# at the end of the setup function
::maneuver::connect_port { local state remote pom/frame/robot }
::maneuver::set_velocity_limit {v 2 w 1}
::nhfc::connect_port { local reference remote maneuver/desired }

# at the end of the start function
::maneuver::set_bounds -- -100 100 -100 100 -2 30 -10 10
::maneuver::set_current_state
::maneuver::take_off { height 0.25 duration 0 }

and in the eltclsh interactive shell, after the setup and start:

# do not use ::nhfc::set_position
# use instead ::maneuver::goto or launch the proskill-drone-hippo

When all these components have beens installed, the proskill-drone-hippo binary can be compiled and run. Just launch it after the simulation has been launched and the drone setup.

Known Problems

Too many to list them here ;-)

This code is largely based on OpenPRS code (parser, etc). It is really a quick and dirty implementation to be a proof of concept, nothing more.

Reporting Problems / Getting Help

Mail: felix@laas.fr