Avis is the aerial vehicle in situ model checker.

Just run make.

Run bin/avis. The following environment variables must be set:

• ARDUPILOT_SRC_PATH - the path to the source code of ArduPilot
• ARDUPILOT_GZ_PATH - the path to the source code of ArduPilot's Gazebo plugin
• PX4_PATH - the path to the source code of PX4

Optionally, AVIS_DEBUG can be set to any value to enable verbose output.

Run make test-unit.

Run make test-functional.

GRPC is used for the workload to interact with RMCK. To obtain the needed programs, run:

$ go get -u google.golang.org/protobuf/cmd/protoc-gen-go
$ go install google.golang.org/protobuf/cmd/protoc-gen-go
$ go get google.golang.org/grpc/cmd/protoc-gen-go-grpc
$ go install google.golang.org/grpc/cmd/protoc-gen-go-grpc

• Metrics server for interesting stats (e.g. # of synthetic readings, etc)