Try an example - VerifiableRobotics/LTL_stack GitHub Wiki
- Download the repo into your workspace src folder:
git clone https://github.com/VerifiableRobotics/LTL_stack.git
catkin_make
your workspace to make sure LTL_stack can be found.- Make sure the files in LTL_stack are all executable:
find <dir to LTL_stack> -type f -exec chmod 755 {} \;
<dir to LTL_stack>
is the directory to your LTL_stack folder. - Try a simple example by running
roslaunch controller_executor tutorial_all.launch
. You should see windows below. - Click the run_executor button to start execution (The button turns green). Turtlesim should start spinning.
- Now if you click the sense_object button (The button turns green), Turtlesim should stop. Green is True and Red is False here. The grey box indicates the values of each proposition.
- You are done! If you want to know more about what each file is doing, you can find more information below.
What's in the example folder
File | Description |
---|---|
setup_launch_tutorial.yaml | Config file to automatically generate all the launch files. |
tutorial.slugsin | LTL specification in slugs format. |
tutorial.yaml | Define how each proposition corresponds to a ROS file. It also specifies the topic of each proposition. |
tutorial_background.launch | Launch nodes other than proposition nodes. |
tutorial_executor.launch | Take in the LTL specification, synthesize a controller and execute it with slugs. |
tutorial_propositions.launch | Launch all the proposition files as defined in simple.yaml. |
tutorial_all.launch | Launch all the other launch files in the folder. An easy way to start running the example. |