Adding fastslow into development

src/examples/testing/fastslow/configs/twoRegions.config

@@ -0,0 +1,55 @@
+# This is a configuration definition file in folder "/home/catherine/Dropbox/ASL/ltlMultiRobot/configs".
+# Format details are described at the beginning of each section below.
+
+
+======== General Config ========
+
+Actuator_Proposition_Mapping: # Mapping between actuator propositions and actuator handler functions
+camera = share.DummyActuatorHandler.setActuator(name="camera")
+
+Initial_Truths: # Initially true propositions
+
+Main_Robot: # The name of the robot used for moving in this config
+Basic_Simulated_Robot
+
+Name: # Configuration name
+twoRegions
+
+Region_Tags: # Mapping from tag names to region groups, for quantification
+{}
+
+Sensor_Proposition_Mapping: # Mapping between sensor propositions and sensor handler functions
+r1_rc = share.DummySensorHandler.inRegion(regionName="r1")
+r2_rc = share.DummySensorHandler.inRegion(regionName="r2")
+camera_ac = share.DummySensorHandler.buttonPress(button_name="camera_ac",init_value=False)
+person = share.DummySensorHandler.buttonPress(button_name="person",init_value=False)
+
+
+======== Robot1 Config ========
+
+CalibrationMatrix: # 3x3 matrix for converting coordinates, stored as lab->map
+array([[1, 0, 0],
+       [0, 1, 0],
+       [0, 0, 1]])
+
+DriveHandler: # Input value for robot drive handler, refer to file inside the handlers/drive folder
+share.Drive.HolonomicDriveHandler(multiplier=50.0,maxspeed=999.0)
+
+InitHandler: # Input value for robot init handler, refer to the init file inside the handlers/robots/Type folder
+basicSim.BasicSimInitHandler(init_region="r1")
+
+LocomotionCommandHandler: # Input value for robot locomotion command handler, refer to file inside the handlers/robots/Type folder
+basicSim.BasicSimLocomotionCommandHandler(speed=0.5)
+
+MotionControlHandler: # Input value for robot motion control handler, refer to file inside the handlers/motionControl folder
+share.MotionControl.VectorControllerHandler()
+
+PoseHandler: # Input value for robot pose handler, refer to file inside the handlers/pose folder
+basicSim.BasicSimPoseHandler()
+
+RobotName: # Robot Name
+Basic_Simulated_Robot
+
+Type: # Robot type
+basicSim
+

src/examples/testing/fastslow/testFastslow.slugsin

@@ -0,0 +1,37 @@
+[INPUT]
+person
+camera_ac
+sbit0
+
+[OUTPUT]
+camera
+bit0
+
+[ENV_TRANS]
+| & ! ! sbit0' ! ! sbit0' & ! sbit0' ! sbit0'
+| ! sbit0' sbit0'
+| ! & ! sbit0 ! bit0 ! sbit0'
+| ! & sbit0 bit0 sbit0'
+| ! & camera_ac camera camera_ac'
+| ! & ! camera_ac ! camera ! camera_ac'
+
+[ENV_LIVENESS]
+| ! ! bit0 ! sbit0'
+| ! bit0 sbit0'
+
+[ENV_INIT]
+! sbit0
+! camera_ac
+
+[SYS_TRANS]
+| ! person' camera'
+| ! camera_ac camera'
+
+[SYS_LIVENESS]
+! sbit0'
+sbit0'
+
+[SYS_INIT]
+bit0
+| ! bit0 bit0
+

src/examples/testing/fastslow/testFastslow.spec

@@ -0,0 +1,67 @@
+# This is a specification definition file for the LTLMoP toolkit.
+# Format details are described at the beginning of each section below.
+
+
+======== SETTINGS ========
+
+Actions: # List of action propositions and their state (enabled = 1, disabled = 0)
+camera, 1
+
+CompileOptions:
+convexify: True
+parser: ltl
+symbolic: False
+use_region_bit_encoding: True
+synthesizer: slugs
+fastslow: True
+decompose: True
+
+CurrentConfigName:
+twoRegions
+
+Customs: # List of custom propositions
+
+RegionFile: # Relative path of region description file
+twoRegions.regions
+
+Sensors: # List of sensor propositions and their state (enabled = 1, disabled = 0)
+person, 1
+
+
+======== SPECIFICATION ========
+
+RegionMapping: # Mapping between region names and their decomposed counterparts
+r1 = p2
+r2 = p1
+others = 
+
+Spec: # Specification in structured English
+# SPEC
+# visit r1 and r2 infinitely often
+# camera stays on once it is turned on
+# camera is triggered when sensing a person
+(e.r1_rc & ! e.camera_ac)
+
+[](next(e.r1_rc) <-> !next(e.r2_rc))
+
+[](next(e.r1_rc) | next(e.r2_rc))
+
+[]((e.r1_rc & s.r1)-> next(e.r1_rc))
+[]((e.r2_rc & s.r2)-> next(e.r2_rc))
+
+[]<>(s.r1  -> next(e.r1_rc))
+[]<>(s.r2  -> next(e.r2_rc))
+
+
+[]((e.camera_ac & s.camera) -> next(e.camera_ac))
+[]((!e.camera_ac & !s.camera) -> !next(e.camera_ac))
+
+--
+s.r2
+
+[] (next(e.person) -> next(s.camera))
+[] (e.camera_ac -> next(s.camera))
+
+[]<> (e.r1_rc)
+[]<> (e.r2_rc)
+

src/examples/testing/fastslow/twoRegions.regions

@@ -0,0 +1,128 @@
+# This is a region definition file for the LTLMoP toolkit.
+# Format details are described at the beginning of each section below.
+# Note that all values are separated by *tabs*.
+
+Background: # Relative path of background image file
+None
+
+CalibrationPoints: # Vertices to use for map calibration: (vertex_region_name, vertex_index)
+
+Obstacles: # Names of regions to treat as obstacles
+
+Regions: # Stored as JSON string
+[
+    {
+        "name": "boundary", 
+        "color": [
+            0, 
+            255, 
+            0
+        ], 
+        "holeList": [], 
+        "height": 0.0, 
+        "points": [
+            [
+                0.0, 
+                3.0
+            ], 
+            [
+                283.0, 
+                3.0
+            ], 
+            [
+                287, 
+                2
+            ], 
+            [
+                580.0, 
+                0.0
+            ], 
+            [
+                576.0, 
+                290.0
+            ], 
+            [
+                283.0, 
+                260.0
+            ], 
+            [
+                0.0, 
+                260.0
+            ]
+        ], 
+        "position": [
+            111.0, 
+            218.0
+        ], 
+        "type": "poly", 
+        "size": [
+            580.0, 
+            290.0
+        ]
+    }, 
+    {
+        "name": "r2", 
+        "color": [
+            0, 
+            0, 
+            255
+        ], 
+        "holeList": [], 
+        "height": 0, 
+        "points": [
+            [
+                0.0, 
+                3.0
+            ], 
+            [
+                4.0, 
+                2.0
+            ], 
+            [
+                297, 
+                0
+            ], 
+            [
+                293, 
+                290
+            ], 
+            [
+                0.0, 
+                260.0
+            ]
+        ], 
+        "position": [
+            394.0, 
+            218.0
+        ], 
+        "type": "poly", 
+        "size": [
+            297.0, 
+            290.0
+        ]
+    }, 
+    {
+        "name": "r1", 
+        "color": [
+            255, 
+            255, 
+            0
+        ], 
+        "height": 0, 
+        "position": [
+            111.0, 
+            221.0
+        ], 
+        "type": "rect", 
+        "size": [
+            283.0, 
+            257.0
+        ]
+    }
+]
+
+Transitions: # Region 1 Name, Region 2 Name, Bidirectional transition faces (face1_x1, face1_y1, face1_x2, face1_y2, face2_x1, ...)
+boundary	r2	398.0	220.0	394.0	221.0	687.0	508.0	394.0	478.0	398.0	220.0	691.0	218.0	687.0	508.0	691.0	218.0
+boundary	r1	394.0	221.0	111.0	221.0	111.0	478.0	394.0	478.0	111.0	478.0	111.0	221.0
+r2	r1	394.0	221.0	394.0	478.0
+

src/examples/testing/structuredFastSlow/configs/basicSim.config

@@ -0,0 +1,59 @@
+# This is a configuration definition file in folder "/home/catherine/LTLMoP/src/examples/testing/structuredFastSlow/configs".
+# Format details are described at the beginning of each section below.
+
+
+======== General Config ========
+
+Actuator_Proposition_Mapping: # Mapping between actuator propositions and actuator handler functions
+gripper = share.DummyActuatorHandler.setActuator(name='gripper')
+camera = share.DummyActuatorHandler.setActuator(name='camera')
+
+Initial_Truths: # Initially true propositions
+
+Main_Robot: # The name of the robot used for moving in this config
+Basic_Simulated_Robot
+
+Name: # Configuration name
+basicSim
+
+Region_Tags: # Mapping from tag names to region groups, for quantification
+{}
+
+Sensor_Proposition_Mapping: # Mapping between sensor propositions and sensor handler functions
+r3_rc = share.DummySensorHandler.inRegion(regionName=u'r3')
+r1_rc = share.DummySensorHandler.inRegion(regionName=u'r1')
+ball = share.DummySensorHandler.buttonPress(button_name='ball', init_value=False)
+r2_rc = share.DummySensorHandler.inRegion(regionName=u'r2')
+camera_ac = share.DummySensorHandler.buttonPress(button_name='camera_ac', init_value=False)
+person = share.DummySensorHandler.buttonPress(button_name='person', init_value=False)
+gripper_ac = share.DummySensorHandler.buttonPress(button_name='gripper_ac', init_value=False)
+
+
+======== Robot1 Config ========
+
+CalibrationMatrix: # 3x3 matrix for converting coordinates, stored as lab->map
+array([[1, 0, 0],
+       [0, 1, 0],
+       [0, 0, 1]])
+
+DriveHandler: # Input value for robot drive handler, refer to file inside the handlers/drive folder
+share.Drive.HolonomicDriveHandler(multiplier=50.0,maxspeed=999.0)
+
+InitHandler: # Input value for robot init handler, refer to the init file inside the handlers/robots/Type folder
+basicSim.BasicSimInitHandler(init_region="r1")
+
+LocomotionCommandHandler: # Input value for robot locomotion command handler, refer to file inside the handlers/robots/Type folder
+basicSim.BasicSimLocomotionCommandHandler(speed=1.0)
+
+MotionControlHandler: # Input value for robot motion control handler, refer to file inside the handlers/motionControl folder
+share.MotionControl.VectorControllerHandler()
+
+PoseHandler: # Input value for robot pose handler, refer to file inside the handlers/pose folder
+basicSim.BasicSimPoseHandler()
+
+RobotName: # Robot Name
+Basic_Simulated_Robot
+
+Type: # Robot type
+basicSim
+