Updated Installation Guide

Step 1: code generation

    cd C
    pc -proj:FlightSystem.pproj

Step 2: build P language C static library

    cd Ext/P/Src
    cmake -DCMAKE_INSTALL_PREFIX=../../../build/P/install -B../../../build/P -H.
    cmake --build ../../../build/P

Step 3: build MAVLink headers

    # refer to https://github.com/mavlink/mavlink
    cd Ext/mavlink
    cmake -H. -DCMAKE_INSTALL_PREFIX=../../build/mavlink/install -B../../build/mavlink -DMAVLINK_DIALECT=ardupilotmega -DMAVLINK_VERSION=2.0
    cmake --build ../../build/mavlink --target install

Step 4: build FlightSystem C program

    mkdir -p build/FlightSystem
    cd build/FlightSystem
    cmake -DCMAKE_PREFIX_PATH=../mavlink/install/lib/cmake/MAVLink/ ../../C
    make -j$(nproc --all)

Pitfall

sometimes when things are being sent, nothing will be displayed on the screen.
monitor the output of MAVproxy or enable the receive_some function in the FlightSystem

PFlight

The field of robotics is ever growing with state spaces exploding due to their complexity. With increasing complexity and the asynchronous nature of modern programs, comes the demand for more robust testing. Current unit testing methods only cover a portion of code, do not efficiently search the entire state space, and often leave interleavings due to concurrency untested. The P programming language is a modeling language and set of associated tools aimed at helping to create modular and safe distributed systems.

P is a state machine based programming language for modeling and specifying complex distributed systems. P allows programmers to model their system as a collection of communicating state machines. P supports several backend analysis engines such as model checking and symbolic execution. P can be systematically tested and compiled into executable code. Combining P with MavSDK, which is a collection of libraries to interface with the MAVLink drone messaging framework, creates a powerful simulation and testing environment for drone robotics systems. MavSDK can manage one or more vehicles via MAVLink. MavSDK communicates with the PX4 flight stack and all testing is done against PX4. Coupled with QGroundControl, a full simulation environment can be set up to test a distributed drone system before real-world deployment.

State machine of a drone using MAVSDK and the P programming language.

Prerequisites

MAVSDK 1.4.4
VUISIS/P 1.1.4
DOTNET 3.1

Build

Clone Repo

git clone git@github.com:VUISIS/PFlight.git --recursive

Ubuntu 20.04:

Install Dotnet

wget https://packages.microsoft.com/config/ubuntu/21.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb
sudo dpkg -i packages-microsoft-prod.deb
rm packages-microsoft-prod.deb

sudo apt-get update; \
sudo apt-get install -y apt-transport-https && \
sudo apt-get update && \
sudo apt-get install -y dotnet-sdk-3.1

Install Java

sudo apt install default-jre

Install P & Coyote

dotnet tool install --global P --version 1.1.4
dotnet tool install --global Microsoft.Coyote.CLI --version 1.0.5

Build P C# Program

cd CSharp
pc -proj:FlightSystem.pproj

Run Test Program Cases

coyote test ./POutput/netcoreapp3.1/FlightSystem.dll -m PImplementation.CheckDroneState.Execute -i 1 -v

coyote test ./POutput/netcoreapp3.1/FlightSystem.dll -m PImplementation.FailDroneState.Execute -i 1 -v

Build P C Program

cd C
pc -proj:FlightSystem.pproj

Install CMake

sudo apt install cmake

Install Python3 Future

pip3 install future

Note: Install globally. May need sudo.

Build MavSDK

cd Ext/MAVSDK
cmake -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=../../build/MAVSDK/install -B../../build/MAVSDK -H.
cmake --build ../../build/MAVSDK --target install

Build P C Static Library

cd Ext/P/Src
cmake -DCMAKE_INSTALL_PREFIX=../../../build/P/install -B../../../build/P -H.
cmake --build ../../../build/P

Build FlightSystem C Program

mkdir -p build/FlightSystem
cd build/FlightSystem
cmake -DCMAKE_PREFIX_PATH=../MAVSDK/install/lib/cmake/MAVSDK ../../C
make -j$(nproc --all)

Running Simulation

Install Docker 
https://docs.docker.com/engine/install/ubuntu/

Install & Run QGroundControl 
https://docs.qgroundcontrol.com/master/en/getting_started/download_and_install.html

Run PX4 Docker
docker run --rm -it --env PX4_HOME_LAT=36.144809502492656 --env PX4_HOME_LON=-86.79316508433672 --env PX4_HOME_ALT=5.0 jonasvautherin/px4-gazebo-headless:1.12.1

Run FlightSystem 
build/FlightSystem/FlightSystem

Running With Docker