Merge pull request #5 from Formal-Systems-Laboratory/cleanup

Cleanup

.clang-format

@@ -0,0 +1,68 @@
+---
+# Taken from: https://github.com/davetcoleman/roscpp_code_format/blob/master/.clang-format
+
+BasedOnStyle:  Google
+AccessModifierOffset: -2
+ConstructorInitializerIndentWidth: 2
+AlignEscapedNewlinesLeft: false
+AlignTrailingComments: true
+AllowAllParametersOfDeclarationOnNextLine: false
+AllowShortIfStatementsOnASingleLine: false
+AllowShortLoopsOnASingleLine: false
+AllowShortFunctionsOnASingleLine: None
+AllowShortLoopsOnASingleLine: false
+AlwaysBreakTemplateDeclarations: true
+AlwaysBreakBeforeMultilineStrings: false
+BreakBeforeBinaryOperators: false
+BreakBeforeTernaryOperators: false
+BreakConstructorInitializersBeforeComma: true
+BinPackParameters: true
+ColumnLimit:    120
+ConstructorInitializerAllOnOneLineOrOnePerLine: true
+DerivePointerBinding: false
+PointerBindsToType: true
+ExperimentalAutoDetectBinPacking: false
+IndentCaseLabels: true
+MaxEmptyLinesToKeep: 1
+NamespaceIndentation: None
+ObjCSpaceBeforeProtocolList: true
+PenaltyBreakBeforeFirstCallParameter: 19
+PenaltyBreakComment: 60
+PenaltyBreakString: 1
+PenaltyBreakFirstLessLess: 1000
+PenaltyExcessCharacter: 1000
+PenaltyReturnTypeOnItsOwnLine: 90
+SpacesBeforeTrailingComments: 2
+Cpp11BracedListStyle: false
+Standard:        Auto
+IndentWidth:     2
+TabWidth:        2
+UseTab:          Never
+IndentFunctionDeclarationAfterType: false
+SpacesInParentheses: false
+SpacesInAngles:  false
+SpaceInEmptyParentheses: false
+SpacesInCStyleCastParentheses: false
+SpaceAfterControlStatementKeyword: true
+SpaceBeforeAssignmentOperators: true
+ContinuationIndentWidth: 4
+SortIncludes: false
+SpaceAfterCStyleCast: false
+
+# Configure each individual brace in BraceWrapping
+BreakBeforeBraces: Custom
+
+# Control of individual brace wrapping cases
+BraceWrapping: {
+    AfterClass: 'true'
+    AfterControlStatement: 'true'
+    AfterEnum : 'true'
+    AfterFunction : 'true'
+    AfterNamespace : 'true'
+    AfterStruct : 'true'
+    AfterUnion : 'true'
+    BeforeCatch : 'true'
+    BeforeElse : 'true'
+    IndentBraces : 'false'
+}
+...

.gitignore

@@ -9,5 +9,7 @@
 
 # Dev artifacts
 tags
-/src/RVMaster/__pycache__/
+__pycache__/
 *~
+*.iml
+

INSTALL.md

@@ -1,35 +1,44 @@
 # Installing ROSRV
 
-Here are instructions for installing and building ROSRV by checking out its 
+Here are instructions for installing and building ROSRV by checking out its
 source code on GitHub.
 
 ## Prerequisites
 
-ROSRV currently works with ROS Groovy Galapagos release. For monitoring 
-purposes, ROSRV depends on ROSMOP.
+### Core Prerequisites
 
-1. [Git](http://git-scm.com/book/en/Getting-Started-Installing-Git)
-v.1.8 or higher
- * Check Git is installed properly: run `git` from a terminal.
-2. [ROS Groovy Galapagos](http://wiki.ros.org/groovy)
-3. [ROSMOP](http://fsl.cs.illinois.edu/index.php/ROSMOP)
- * Please check the 
-   [ROSMOP Installation guide](https://github.com/runtimeverification/rosmop/blob/master/INSTALL.md).
+1. [ROS Kinetic](http://wiki.ros.org/kinetic)
+2. [PyTest](https://docs.pytest.org/)
+3. [Maven](https://maven.apache.org)
+4. [Catkin](http://wiki.ros.org/catkin)
+
+### RV-Monitor
+
+1. [RV-Monitor](https://github.com/runtimeverification/rv-monitor)
+    To use RV-Monitor supported logics RV-Monitor install RV-Monitor
+    using the instructions at the tool's page (use `mvn install`
+    to install snapshot to local maven repository).
+    Set environment variable `RVMONITOR` to point to `rv-monitor's`
+    root directory.
 
 ## Install and Build
 
-1. Run `git clone --recursive https://github.com/runtimeverification/ROSRV.git` 
-to check out the source code from the Github repository, including 
-[ROSMOP](https://github.com/runtimeverification/rosmop).
+1. After Installing Prerequisites, run `./Test` to
+   Build and Run Tests.
 
-2. Add `<ROSRV_HOME>/bin` to your PATH.
+2. The default behavior of the testing setup is to run
+   all tests. Use `PYTEST_FLAGS="--skip-dl-tests"` to
+   skip Differential Dynamic Logic based tests.
 
-3. Run 
- * `cd <ROSRV_HOME>`
- * `catkin_make`
+### Running
+ROSRV can simply be treated as a catkin project, and
+dropped into an existing catkin workspace.
 
-4. Make sure the target package builds successfully.
+The `bin/rosrv` provides a wrapper to the
+C++ code generator. For example `bin/rosrv <SPEC_FILE> -o [MONITOR_NAME]`
+will generate a monitor `MONITOR_NAME` which can be run
+via catkin as `catkin run rvmonitor <MONITOR_NAME>`.
 
-See [docs/Usage.md](docs/Usage.md) for information on how to run ROSRV.
+See [docs/Usage.md](docs/Usage.md) for further information on how to run ROSRV.
 Get help or report problems on
-[ROSRV's issues page](https://github.com/runtimeverification/ROSRV/issues).
+[ROSRV's issues page](https://github.com/FormalSystemsLaboratory/ROSRV/issues).

Test

@@ -6,7 +6,7 @@ repo_dir="$(cd "$(dirname "$0")"; pwd)"
 progress() { echo ==== "$@" ; }
 
 trap 'cleanup; echo >&2 "FAILED!"' 0
-cleanup() { progress "Cleaning up"; kill $(jobs -p) >/dev/null 2>&1 || true ; }
+cleanup() { progress "Cleaning up"; kill $(jobs -p) >/dev/null 2>&1 || true ; sleep 1 ; }
 clean_exit() {
     cleanup
     trap '' 0
@@ -27,28 +27,38 @@ progress "Building rosmop"
 (cd src/rosmop ; mvn -q package -DskipTests)
 
 progress "Building src"
-catkin build --cmake-args -DCMAKE_BUILD_TYPE=Debug -DBUILD_TESTING=ON --
+catkin build --cmake-args -DBUILD_TESTS=ON -DCMAKE_BUILD_TYPE=Debug -DBUILD_TESTING=ON --
 
-export ROS_MASTER_URI="http://localhost:11311/"
-export REAL_MASTER_URI="http://localhost:20022/"
-export ACCESS_POLICY_PATH="$repo_dir/config/access-policy.cfg"
-source devel/setup.bash
+test_against_rvmaster() {
+    export ROS_MASTER_URI="http://localhost:11311/"
+    export REAL_MASTER_URI="http://localhost:20022/"
+    export ACCESS_POLICY_PATH="$repo_dir/config/access-policy.cfg"
+
+    progress "Running roscore"
+    ROS_MASTER_URI="$REAL_MASTER_URI" roscore -p 20022  >/dev/null &
+    sleep 1
+
+    progress "Running Simple Tests With RVMaster"
+    pytest --with-rvmaster "$PYTEST_FLAGS" t/test_monitors.py
 
-progress "Running roscore"
-ROS_MASTER_URI="$REAL_MASTER_URI" roscore -p 20022  >/dev/null &
-sleep 1
+    cleanup
+}
 
-progress "Running rvmaster"
-rosrun rvmaster rvmaster >/dev/null &
-sleep 1
+test_without_rvmaster() {
+    export ROS_MASTER_URI="http://localhost:20022/"
+    export ACCESS_POLICY_PATH="$repo_dir/config/access-policy.cfg"
 
-monitor=testSpecOne
-progress "Enabling $monitor"
-bin/rosrv.py -enable "$monitor" >/dev/null
-bin/rosrv.py -list "$monitor"
-sleep 1
+    progress "Running roscore"
+    roscore -p 20022 >/dev/null  &
+    sleep 1
 
-progress "Running tests"
-pytest ./src/RVMaster/test-monitors.py
+    progress "Running Simple Tests Without RVMaster"
+    pytest "$PYTEST_FLAGS" t/test_monitors.py
 
+    cleanup
+}
+
+source devel/setup.bash
+( progress test_without_rvmaster ; test_without_rvmaster )
+( progress test_against_rvmaster ; test_against_rvmaster )
 clean_exit 0

bin/rosrv

@@ -1,4 +1,33 @@
-#!/bin/bash
-SHDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+#!/usr/bin/python2
+
+from __future__ import print_function
+import argparse, os, sys
+from subprocess import check_call
+
+parser = argparse.ArgumentParser(description='ROSRV Monitor Node Generator')
+
+parser.add_argument( 'spec_file'
+		   , help='The location of the spec file'
+		   )
+
+parser.add_argument( '-o', '--output'
+		   , help='Name of the monitor executable'
+		   )
+
+args = parser.parse_args()
+
+# Check File Exists
+if not os.path.exists(args.spec_file):
+    print(args.spec_file + " Spec File not found", file=sys.stderr)
+    sys.exit(1)
+
+
+spec_file_path = os.path.abspath(args.spec_file)
+if args.output:
+    check_call( ['/usr/bin/env', 'catkin', 'build', 'rvmonitor'
+  	      , ('-DPROVIDED_SPEC_FILE=' + spec_file_path)
+  	      , ('-DPROVIDED_MONITOR_NAME=' + args.output) ])
+else:
+    check_call( ['/usr/bin/env', 'catkin', 'build', 'rvmonitor'
+              , ('-DPROVIDED_SPEC_FILE=' + spec_file_path) ])
 
-python $SHDIR/rosrv.py $@

src/RVMaster/CMakeLists.txt

@@ -4,26 +4,17 @@ set(CMAKE_CXX_STANDARD 11)
 
 ## ROS Master
 
-add_custom_command(
-    OUTPUT ${PROJECT_BINARY_DIR}/monitor/rvmonitor.cpp
-           ${PROJECT_BINARY_DIR}/monitor/rvmonitor.h
-    COMMAND mkdir -p ${PROJECT_BINARY_DIR}/monitor/ &&
-            rosmop --output-prefix ${PROJECT_BINARY_DIR}/monitor/rvmonitor
-                   ${PROJECT_SOURCE_DIR}/rvmonitor.rv
-    DEPENDS rvmonitor.rv
-)
-include_directories(${PROJECT_BINARY_DIR}/monitor/)
-
 get_filename_component(PARENT_DIR ${CMAKE_SOURCE_DIR} PATH)
 
 find_package(catkin REQUIRED COMPONENTS roscpp rospy)
+catkin_package( INCLUDE_DIRS include
+                DEPENDS rvmonitor
+              )
 find_package(Boost REQUIRED COMPONENTS regex program_options)
-catkin_package( INCLUDE_DIRS include )
 
 include_directories(include/ ${catkin_INCLUDE_DIRS} ${Boost_INCLUDE_DIR} )
 
 add_library( librvmaster
-             ${PROJECT_BINARY_DIR}/monitor/rvmonitor.cpp
              src/xmlrpcpp/XmlRpcClient.cpp
              src/xmlrpcpp/XmlRpcServerConnection.cpp
              src/xmlrpcpp/XmlRpcServerMethod.cpp
@@ -32,36 +23,15 @@ add_library( librvmaster
              src/xmlrpcpp/XmlRpcSource.cpp
              src/xmlrpcpp/XmlRpcDispatch.cpp
              src/rv/xmlrpc_manager.cpp
-             src/rv/connection_manager.cpp
-             src/rv/transport_publisher_link.cpp
-             src/rv/transport_subscriber_link.cpp
-             src/rv/subscription.cpp
-             src/rv/publisher_link.cpp
              src/rv/server_manager.cpp
              src/rv/master.cpp
              src/rv/acctrl_manager.cpp
-             src/rv/monitor.cpp
            )
 target_link_libraries(librvmaster ${catkin_LIBRARIES} ${Boost_LIBRARIES} )
 
 add_executable(rvmaster src/main.cpp)
 target_link_libraries(rvmaster librvmaster)
 
-## Isolated monitor
-
-add_custom_command(
-    OUTPUT ${PROJECT_BINARY_DIR}/isolated-monitor/rvmonitor.cpp
-           ${PROJECT_BINARY_DIR}/isolated-monitor/rvmonitor.h
-    COMMAND mkdir -p ${PROJECT_BINARY_DIR}/isolated-monitor/ &&
-            rosmop --output-prefix ${PROJECT_BINARY_DIR}/isolated-monitor/rvmonitor
-                   --monitor-as-node
-                   ${PROJECT_SOURCE_DIR}/rvmonitor.rv
-    DEPENDS rvmonitor.rv
-)
-add_executable(test-isolated-monitor ${PROJECT_BINARY_DIR}/isolated-monitor/rvmonitor.cpp)
-target_include_directories(test-isolated-monitor PRIVATE ${PROJECT_BINARY_DIR}/isolated-monitor/)
-target_link_libraries(test-isolated-monitor ${catkin_LIBRARIES} ${Boost_LIBRARIES})
-
 ## Install
 
 install( TARGETS rvmaster