Try an example

1. Download the repo into your workspace src folder: git clone https://github.com/VerifiableRobotics/LTL_stack.git
2. catkin_make your workspace to make sure LTL_stack can be found.
3. 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.
4. Try a simple example by running roslaunch controller_executor tutorial_all.launch. You should see windows below.
5. Click the run_executor button to start execution (The button turns green). Turtlesim should start spinning.
6. 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.
7. 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.