Permalink
Browse files

Merge remote-tracking branch 'vasu/fixEg' into development

  • Loading branch information...
2 parents 7e00d70 + da17f60 commit a168dfab0ba043b3ed523c707ef90f909bbe0841 @cfinucane cfinucane committed Apr 18, 2012
@@ -1,106 +0,0 @@
-# This is a specification 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*.
-
-
-======== EXPERIMENT CONFIG 0 ========
-
-Calibration: # Coordinate transformation between map and experiment: XScale, XOffset, YScale, YOffset
-0.0145090906457,-7.97493804517,-0.0163607845119,5.97177404282
-
-InitialRegion: # Initial region number
-0
-
-InitialTruths: # List of initially true propositions
-
-Lab: # Lab configuration file
-playerstage.lab
-
-Name: # Name of the experiment
-PlayerStage
-
-RobotFile: # Relative path of robot description file
-pioneer_stage.robot
-
-
-======== EXPERIMENT CONFIG 1 ========
-
-Calibration: # Coordinate transformation between map and experiment: XScale, XOffset, YScale, YOffset
-0.00667619043562,0.519140956528,-0.00536700273334,2.25351186904
-
-InitialRegion: # Initial region number
-0
-
-InitialTruths: # List of initially true propositions
-
-Lab: # Lab configuration file
-cornell_asl.lab
-
-Name: # Name of the experiment
-ASL
-
-RobotFile: # Relative path of robot description file
-pioneer_real.robot
-
-
-======== SETTINGS ========
-
-Actions: # List of actions and their state (enabled = 1, disabled = 0)
-pick_up,1
-drop,1
-radio,1
-extinguish,0
-
-Customs: # List of custom propositions
-carrying_item
-
-RegionFile: # Relative path of region description file
-debug.regions
-
-Sensors: # List of sensors and their state (enabled = 1, disabled = 0)
-fire,0
-person,1
-hazardous_item,1
-
-currentExperimentName:
-ASL
-
-
-======== SPECIFICATION ========
-
-RegionMapping:
-
-living=p5
-deck=p8
-porch=p4
-dining=p19,p20
-bedroom=p9
-others=p10,p11,p12,p13,p14,p15,p16,p17,p18
-kitchen=p6
-
-Spec: # Specification in simple English
-Env starts with false
-Robot starts in deck
-Robot starts with false
-If you were in porch then do person
-If you were in porch then do not hazardous_item
-Do pick_up if and only if you are sensing hazardous_item and you are not activating carrying_item
-Do drop if and only if you are activating carrying_item and you were in porch
-If you are activating pick_up or you activated pick_up then stay there
-If you are activating drop or you activated drop then stay there
-Do radio if and only if you are sensing person
-If you are activating radio or you activated radio then stay there
-If you activated pick_up then do carrying_item
-If you activated drop and you did not activate pick_up then do not carrying_item
-If you activated carrying_item and you did not activate drop then do carrying_item
-If you did not activate carrying_item and you did not activate pick_up then do not carrying_item
-#If you are not activating carrying_item and you are not activating radio then visit dining
-If you are not activating carrying_item and you are not activating radio then visit deck
-always not living
-If you are not activating carrying_item and you are not activating radio then visit living
-If you are not activating carrying_item and you are not activating radio then visit bedroom
-If you are not activating carrying_item and you are not activating radio then visit kitchen
-If you did not activate carrying_item then always not porch
-If you are activating carrying_item and you are not activating radio then visit porch
-
-
@@ -1,36 +0,0 @@
-# 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)
-boundary 0
-dining 5
-
-Regions: # Name, Type, Pos X, Pos Y, Width, Height, Color R, Color G, Color B, Vertices (x1, y1, x2, y2, ...)
-boundary poly 58 80 1041 657 160 32 240 0 0 241 0 813 0 1041 0 1040 494 907 657 361 657 237 496 0 503
-kitchen poly 295 328 224 248 255 165 0 4 0 224 2 224 3 224 4 224 233 224 234 223 241 0 248
-porch poly 58 80 241 503 255 255 0 0 0 241 0 241 239 241 240 241 248 237 496 0 503
-deck poly 295 569 803 168 0 255 1 576 0 803 5 670 168 124 168 0 7 223 0
-bedroom poly 871 80 228 494 139 76 132 0 240 0 0 228 0 227 494 0 489
-dining poly 519 320 346 243 255 247 0 0 242 0 241 0 12 0 11 0 10 0 1 0 0 345 0 346 243
-living poly 299 80 572 240 233 123 19 0 239 0 0 572 0 572 240 565 240 220 240 0 240
-
-Thumbnail: # Relative path of image file that has region shapes overlayed on background image
-iros10_simbg.png
-
-Transitions: # Region 1 Name, Region 2 Name, Bidirectional transition faces (face1_x1, face1_y1, face1_x2, face1_y2, face2_x1, ...)
-boundary porch 58 80 58 583 58 583 295 576 58 80 299 80
-boundary deck 965 737 1098 574 295 576 419 737 419 737 965 737
-boundary bedroom 1098 574 1099 80 871 80 1099 80
-boundary living 299 80 871 80
-kitchen porch 295 576 299 328
-kitchen deck 295 576 518 569
-kitchen dining 519 330 519 331 519 332 519 561 519 331 519 332 519 561 519 562
-porch living 299 319 299 320 299 80 299 319
-deck bedroom 871 569 1098 574
-bedroom living 871 80 871 320
-dining living 519 320 864 320
-
@@ -19,7 +19,7 @@ kitchen poly 299 320 220 255 255 0 0 0 0 220 11 220 241 219 249 0 255
boundary poly 13 10 1183 729 0 0 255 35 576 0 14 131 17 211 20 420 0 1106 34 1183 616 954 729 402 729
Thumbnail: # Relative path of image file that has region shapes overlayed on background image
-debug_simbg.png
+unsynth_simbg.png
Transitions: # Region 1 Name, Region 2 Name, Bidirectional transition faces (face1_x1, face1_y1, face1_x2, face1_y2, face2_x1, ...)
porch living 299 80 299 320
@@ -54,7 +54,7 @@ extinguish,0
Customs: # List of custom propositions
RegionFile: # Relative path of region description file
-iros10.regions
+unsynth.regions
Sensors: # List of sensors and their state (enabled = 1, disabled = 0)
fire,1
@@ -69,15 +69,18 @@ ASL
RegionMapping:
-living=p4
-porch=p3
-deck=p7
-others=p2,p9,p10
-dining=p6
-bedroom=p8
-kitchen=p5
+living=p5
+deck=p8
+porch=p4
+dining=p19,p20
+bedroom=p9
+others=p10,p11,p12,p13,p14,p15,p16,p17,p18
+kitchen=p6
Spec: # Specification in simple English
+#Simple specification demonstrating liveness unrealizability
+#Environment can win by alternating fire and person
+
Env starts with false
Robot starts with false
Robot starts in deck
@@ -55,7 +55,7 @@ Customs: # List of custom propositions
carrying_item
RegionFile: # Relative path of region description file
-debug.regions
+unsynth.regions
Sensors: # List of sensors and their state (enabled = 1, disabled = 0)
fire,1
@@ -79,74 +79,75 @@ others=p10,p11,p12,p13,p14,p15,p16,p17,p18
kitchen=p6
Spec: # Specification in simple English
-Env starts with false
-Robot starts with not drop
-If you activated drop and you are sensing fire then do not drop
-If you activated drop and you are sensing fire then do drop
-If you did not activate drop then do drop
-
-#Do pick_up if and only if you are sensing hazardous_item
-#Do drop if and only if you were in porch
-#If you are activating pick_up or you activated pick_up then stay there
-#If you are activating drop or you activated drop then stay there
-#If you did not activate pick_up then always not porch
-#Visit porch
-#Always person and not person
-
-
-
-
-
+#SIMPLE EXAMPLES OF EACH CASE OF UNSYNTHESIZABILITY:
+##############################################
+##UNSATISFIABLE
+##############################################
+##System safety unsatisfiable -- single step
+#Env starts with false
+#Robot starts in deck
+#Always porch
+##Environment safety unsatisfiable -- single step
+#Env starts with false
+#Robot starts in deck
+#Always person and not person
+##Multi-step unsatisfiability
+Env starts with false
+Robot starts with not drop
+If you activated drop then do not drop
+If you activated drop then do drop
+If you did not activate drop then do drop
+##############################################
+##System liveness and safety unsatisfiable
+#Env starts with false
+#Robot starts in deck
+#Always not porch
+#Infinitely often porch
+##Environment liveness and safety unsatisfiable
+#Env starts with false
+#Robot starts in deck
+#Always not person
+#Infinitely often person
-#NON-TRIVIAL EXAMPLES:
+##############################################
+##UNREALIZABLE
+##############################################
-#Environment liveness unrealizable
+##System safety unrealizable -- single step
#Env starts with false
-#Robot starts with false
-#robot starts with false
-#If you were in porch then do not hazardous_item
-#If drop then not drop
-#If drop then drop
-#If not drop then drop
-#Do pick_up if and only if you are sensing hazardous_item
-#Do drop if and only if you were in porch
-#If you are activating pick_up or you activated pick_up then go to porch and stay there
-#If you are activating drop or you activated drop then stay there
-#If you did not activate pick_up then always not porch
-#Visit porch
-#If you were in porch then infinitely often person and not person
-#Go to porch and stay there
+#Robot starts in deck
+#Always not porch
+#If you are sensing person then do porch
-##System safety unrealizable
+##Environment safety unrealizable -- single step
#Env starts with false
-#Robot starts in porch
-#If you were in porch then do not hazardous_item
+#Robot starts in deck
+#Always not person
+#If you were in porch then do person
+
+##Multi-step unrealizability
#Do pick_up if and only if you are sensing hazardous_item
#Do drop if and only if you were in porch
#If you are activating pick_up or you activated pick_up then stay there
#If you are activating drop or you activated drop then stay there
#If you did not activate pick_up then always not porch
-#Visit porch
-##If you were in porch then infinitely often person and not person
-
-#SIMPLE EXAMPLES OF EACH CASE:
+##############################################
##System liveness unrealizable
#Env starts with false
#Robot starts in deck
#Visit porch
#If you are sensing person then do not porch
-#Visit person
##Environment liveness unrealizable
#Env starts with false
@@ -156,38 +157,4 @@ If you did not activate drop then do drop
#Visit not person
#If you were in deck then do person
-##System safety unrealizable
-#Env starts with false
-#Robot starts in deck
-#Always not porch
-#If you are sensing person then do porch
-
-##Environment safety unrealizable
-#Env starts with false
-#Robot starts in deck
-#Always not person
-#If you were in porch then do person
-
-##System liveness and safety unsatisfiable
-#Env starts with false
-#Robot starts in deck
-#Always not porch
-#Infinitely often porch
-
-##Environment liveness and safety unsatisfiable
-#Env starts with false
-#Robot starts in deck
-#Always not person
-#Infinitely often person
-
-##System safety unsatisfiable
-#Env starts with false
-#Robot starts in deck
-#Always porch
-
-##Environment safety unsatisfiable
-#Env starts with false
-#Robot starts in deck
-#Always person and not person
-

0 comments on commit a168dfa

Please sign in to comment.