verifiablerobotics/ltlmop

A toolkit for designing and implementing LTL-based task specifications.

ltlmop's Issues

SLURP spec of "Stay there." crashes GROne

Tested in the LTLMoP gumbo branch:

1. Open speceditor with the examples/slurptest/slurptest.spec spec.
2. Change the spec to only say "Stay there."
3. GROne crashes with the following stack:

    Exception in thread "main" net.sf.javabdd.BDDException: ERROR: Cannot prime primed variables: 
        
        at edu.wis.jtlv.env.Env$JTLVBDDManagerPairing.prime(Env.java:3460)
        at edu.wis.jtlv.env.Env$JTLVBDDManagerPairing.access$3(Env.java:3457)
        at edu.wis.jtlv.env.Env.prime(Env.java:1735)
        at edu.wis.jtlv.env.module.Module.yieldStates(Module.java:552)
        at GROneGame.calculate_win(GROneGame.java:131)
        at GROneGame.(GROneGame.java:87)
        at GROneGame.(GROneGame.java:48)
        at GROneMain.main(GROneMain.java:114)

Bare LTL compilation in speceditor fails

It looks like all spec compilation fails when the parser mode is LTL. For example, opening example/firefighting/specInLTL.spec, in the development or gumbo branches and compiling leads to:

Decomposing map into convex regions...
    Traceback (most recent call last):
      File "specEditor.py", line 1068, in onMenuCompile
            compiler._decompose()
      File "lib/specCompiler.py", line 115, in _decompose
            self.parser.proj.rfi.writeFile(filename)
      File "lib/regions.py", line 368, in writeFile
            self.regions[region1 + 1 + region2].name] +
    IndexError  :   list index out of range 

Changing the decomposition options in the spec file and menu doesn't seem to have an effect, but I'm not sure I've tried every possible combination.

use of udp in dummyactuator messaging can result in out of order log

Config files overwritten when saved

After I edited a config file and saved it,

1. CurrentConfigName in .spec sometimes disappear.
2. proposition mappings of the current config file is overwritten if there are other existing config files.

Analyze shows slurptest.spec as unrealizable

Reproduction steps:

1. Checkout latest slurp-dev (cc96ed4).
2. Run python specEditor.py examples/slurptest/slurptest.spec
3. Debug --> Analyze (you can compile first, it doesn't matter)

Expected: Analysis window shows that the spec is okay.
Actual: See "System highlighted goal(s) unrealizable. 1" and red highlighted lines. (Note that there's no pink, that's because of issue #10.) Screenshot:

My only guess was that there's some leftover file from when this same spec was unrealizable in the past?

speceditor last line of text flickers on ubuntu

NLTK parsing of empty/1-item groups gives bad LTL

For example, try:

Group emptygroup is empty
Group oneitemgroup is radio

Visit each emptygroup
Always do any oneitemgroup

This returns:

[]((s.radio | )) & 
([]<>(empty) & ) & ...

simGUI event listener assumes eventData is string

will crash if float/int type is accidentally passed in

Debug/Analyze does not correctly highlight unrealizable cores

I got the following highlight (with LTLMoP/development)

but I think it should be (with vramen/cores)

I can also obtain the same result with the following replacement in specEditor.py:

FROM
#highlight guilty sentences
#special treatment for goals: we already know which one to highlight
if self.proj.compile_options["parser"] == "structured":
for h_item in self.to_highlight:
tb_key = h_item[0].title() + h_item[1].title()
if h_item[1] == "goals":
self.text_ctrl_spec.MarkerAdd(self.tracebackTree[tb_key][h_item[2]]-1, MARKER_LIVE)
elif self.proj.compile_options["parser"] == "slurp":
for frag in self.to_highlight:
tb_key = frag[0].title() + frag[1].title()
self.text_ctrl_spec.MarkerAdd(self.tracebackTree[tb_key][frag[2]]-1, MARKER_LIVE)
self.analysisDialog.markFragments(*frag)
else:
print "Fragment marking not yet supported for this parser type"

TO (copied from varmen/cores' branch)
if not realizable or not nonTrivial:
#only do cores if unrealizable or trivial

            #highlight guilty sentences
            #special treatment for goals: we already know which one to highlight                
            for h_item in self.to_highlight:
                tb_key = h_item[0].title() + h_item[1].title()
                if h_item[1] == "goals":
                    self.text_ctrl_spec.MarkerAdd(self.tracebackTree[tb_key][h_item[2]]-1, MARKER_LIVE)

            if self.unsat:
                guilty = compiler._coreFinding(self.to_highlight, self.unsat, self.badInit)
                self.highlightCores(guilty)
            else:
                #just highlight all sentences in the guilty components
                for h_item in [h for h in self.to_highlight if h[1] != "goals"]:
                        tb_key = h_item[0].title() + h_item[1].title()
                        for l in self.tracebackTree[tb_key]:
                            self.highlight(l, h_item[1])
    """

LTL generation doesn't handle 1-region maps correctly

log_2(1) = 0

Extra & in LTL file if no environment constraints

Reproduction steps:

1. Checkout latest slurp-dev (cc96ed4).
2. Run python specEditor.py examples/slurptest/slurptest_unreal.spec
3. Compile

Expected: Spec compiles but is unrealizable.
Actual: Compilation fails with:

Creating automaton...
    line 10:1 no viable alternative at input ')'
    Exception in thread "main" java.lang.Exception: Cannot parse specification "null".

When I look at the .ltl file, I see:

LTLSPEC -- Assumptions
        (
        TRUE & [](TRUE) & []<>(TRUE)
                &
                
        );

It looks like that extra & is killing it.

You can type on SimGUI log

SimGUI log ca be edited by user. You can move the cursors and the printing to the log will be messed up.

Python issues

LTLMop installer does not find Python 2.6., even if Python has been installed and its path added. (For example, Polygon installer and others finds it ok.)

Operating system: Win 7 64-bit.

New region editor obstacle regions problems

I have created a region map with one region that exists as an 'obstacle.' If I start spec editor and open my spec, then try to start region editor, I get the following:
File "regionEditor.py", line 2517, in
regEd = regionEditor(None, -1, sys.argv[1])
File "regionEditor.py", line 285, in init
self.ReadFile(self.fileName)
File "regionEditor.py, line1551, in ReadFile
regName)].isObstacle = True

Also, after this error happens and I try to edit my region map by starting the region editor manually, the region is now a normal region (and not an 'obstacle').

To fix:
look for this line: self.regions[self.indexOfRegionWithName
make sure the I in index is Capitalized: self.regions[self.IndexOfRegionWithName

handlers in robot files could not be loaded

I am attempting to use a nao robot in the execution environment but it appears the handlers for most robot types could not be loaded from .robot file in handlerSubsystem.py. Do I need to create custom handlers or are these available somewhere? Namely, the init handler is missing for the nao robot. Looking at the init python file in lib/handlers/robots/nao gives me a blank file.

allow speced to run even when CWD is not src/

be friendlier when initial state violates some assumption

e.g. "make a simulation popup: "You specified the simulation should start in region X, but there's no initial state with that region.""

end execution if only possible state successor is current state (regardless of env)

Changing robot configuration requires renaming the robot

It seems that since 8923c7d every time I edit a robot configuration it won't allow me to save it unless I rename the robot. Is this intended?

view aut is broken

Problem with python install script on windows 7

I am using Python 2.7.3 and I get the following error with the setup script

---

C:\Projects\LTLMoP\dist>py setup.py
Trying to use Git Bash...
Found Git Bash at C:\ProgramFiles\Git\bin\bash.exe
Welcome to Git (version 1.8.0-preview20121022)

Run 'git help git' to display the help index.
Run 'git help ' to display help for specific commands.
File "C:\Projects\LTLMoP\dist\setup.py", line 29
print "-> Running command '{} {}'...".format(program, " ".join(args))
^

SyntaxError: invalid syntax

(error marker is pointing at the " just before .format)

robot configuration window too small

on edit robot, handler config buttons are almost invisible

Experimental Configurations

Added Experimental Configurations disappear after hitting apply. (Windows)

Spec Editor trying to parse a comment

It looks like specEditor is trying to parse the commented out sentence in line 24 (see screenshot). It compiles just fine if I delete that comment.

Update: It also compiles if I just delete the word "near".

Setting basicSim init_region in GUI is blank

When I set the initial region for basicSim using the GUI, I seem to always end up with an empty string. If I just edit the file manually to the same region name, things are okay.

basicSimInit(init_region="")

Couldn't find Git Bash (Installation issues)

When I try to run setup.py, I get the error message that it can't find the Git Bash. Attached is an image of my files. They're all in the G:\ directory.

give better error if no simulation config is defined

Sensor proposition name cant start with a number

Sensor proposition 0Button gave error when I ran the spec (sensors starting with numbers could cause issues)

SimGUI not printing out Other Debugging Messages

Current in SimGUI line starting at line 170:

        if isinstance(eventData, basestring):
            if eventData.startswith("Output proposition"):
                if self.checkbox_statusLog_propChange.GetValue():
                    wx.CallAfter(self.appendLog, eventData + "\n", color="GREEN") 
            elif eventData.startswith("Heading to"):
                if self.checkbox_statusLog_targetRegion.GetValue():
                    wx.CallAfter(self.appendLog, eventData + "\n", color="BLUE") 
            elif eventData.startswith("Crossed border"):
                if self.checkbox_statusLog_border.GetValue():
                    wx.CallAfter(self.appendLog, eventData + "\n", color="CYAN") 
                # Detect our current goal index
            elif eventData.startswith("Currently pursuing goal"):
                m = re.search(r"#(\d+)", eventData)
                if m is not None:
                    self.currentGoal = int(m.group(1))
       elif self.checkbox_statusLog_other.GetValue():
           if eventData != "":
                wx.CallAfter(self.appendLog, str(eventData) + "\n", color="BLACK") 

The last three lines should be indented so that optional debugging messages are printed as follows:

        if isinstance(eventData, basestring):
            if eventData.startswith("Output proposition"):
                if self.checkbox_statusLog_propChange.GetValue():
                    wx.CallAfter(self.appendLog, eventData + "\n", color="GREEN") 
            elif eventData.startswith("Heading to"):
                if self.checkbox_statusLog_targetRegion.GetValue():
                    wx.CallAfter(self.appendLog, eventData + "\n", color="BLUE") 
            elif eventData.startswith("Crossed border"):
                if self.checkbox_statusLog_border.GetValue():
                    wx.CallAfter(self.appendLog, eventData + "\n", color="CYAN") 
                # Detect our current goal index
            elif eventData.startswith("Currently pursuing goal"):
                m = re.search(r"#(\d+)", eventData)
                if m is not None:
                    self.currentGoal = int(m.group(1))
           elif self.checkbox_statusLog_other.GetValue():
               if eventData != "":
                    wx.CallAfter(self.appendLog, str(eventData) + "\n", color="BLACK") 

I can submit a pull request if that's correct.

"and" in a handler param causes crash.

how to draw trajectory of robot on screen after simulation

how to draw trajectory of robots on screen after simulation (with different colours for every robots)?

Thanks very much

DEEPPINK color not on all systems

It looks like as much as we like that color it isn't universally supported. On my machine (wxPython on Python 2.7, OS 10.7), I get:
[Debug] 08:12:13: wxColour::Set - couldn't set to colour string 'DEEPPINK'

This color was introduced to specEditor in 3e359fc.

on windows, spec files cannot be on a different drive than the ltlmop directory

Sporadic crashes in controllerListen

I suspect there's a timing issue that leads to this occasional crash:

[ LTLMOP HYBRID CONTROLLER EXECUTION MODULE ]

Hello. Let's do this!

Loading specification file /home/lignos/checkout/LTLMoP/src/examples/slurptest/slurptest.spec...
Loading config file /home/lignos/checkout/LTLMoP/src/examples/slurptest/configs/basicsim.config...
Loading region file /home/lignos/checkout/LTLMoP/src/examples/slurptest/iros10.regions...
  -> Found definitions for 9 regions.
Loading region file /home/lignos/checkout/LTLMoP/src/examples/slurptest/slurptest_decomposed.regions...
  -> Found definitions for 6 regions.
Importing handler functions...
  -> handlers.robots.basicSim.basicSimInit
(Basic Simulator) Initializing Basic Simulator...
(Basic Simulator) Start Basic Simulator...
  -> handlers.pose.basicSimPose
  -> handlers.robots.basicSim.basicSimLocomotionCommand
  -> handlers.drive.holonomicDrive
  -> handlers.motionControl.vectorController
  -> handlers.robots.basicSim.basicSimSensor
  -> handlers.share.dummySensor
  -> handlers.robots.basicSim.basicSimActuator
  -> handlers.share.dummyActuator
(POSE) Initial pose: [ 962.   324.6    0. ]
Starting GUI window and listen thread...
wx is loaded, using wx objects for regions
(GUI) Starting socket for communication to controller
(GUI) Starting socket for communication from controller
(GUI) Starting controller listen thread...
Exception in thread Thread-1:
Traceback (most recent call last):
  File "/usr/lib/python2.7/threading.py", line 551, in __bootstrap_inner
    self.run()
  File "/usr/lib/python2.7/threading.py", line 504, in run
    self.__target(*self.__args, **self.__kwargs)
  File "/home/lignos/checkout/LTLMoP/src/lib/simGUI.py", line 147, in controllerListen
    [x,y] = map(int, (self.mapScale*x, self.mapScale*y))
AttributeError: 'SimGUI_Frame' object has no attribute 'mapScale'```

Scintilla crashes on CallTipShow in SpecEditor with wx2.9.5 (OS X)

Crashed Thread:  0  Dispatch queue: com.apple.main-thread

Exception Type:  EXC_BAD_ACCESS (SIGSEGV)
Exception Codes: EXC_I386_GPFLT

Application Specific Information:
objc_msgSend() selector name: becomeKeyWindow


Thread 0 Crashed:: Dispatch queue: com.apple.main-thread
0   libobjc.A.dylib                 0x00007fff93d92250 objc_msgSend + 16
1   com.apple.AppKit                0x00007fff8c495f04 -[NSWindow _changeKeyAndMainLimitedOK:] + 719
2   com.apple.AppKit                0x00007fff8c49576b -[NSWindow _makeKeyRegardlessOfVisibility] + 104
3   com.apple.AppKit                0x00007fff8c4956c5 -[NSWindow makeKeyAndOrderFront:] + 25
4   libwx_osx_cocoau-2.9.dylib      0x0000000107f0cb4d wxNonOwnedWindowCocoaImpl::Show(bool) + 291
5   libwx_osx_cocoau-2.9.dylib      0x0000000107e6f77b wxNonOwnedWindow::Show(bool) + 57
6   libwx_osx_cocoau-2.9.dylib      0x000000010847a671 ScintillaBase::CallTipShow(Point, char const*) + 537
7   libwx_osx_cocoau-2.9.dylib      0x000000010847af71 ScintillaBase::WndProc(unsigned int, unsigned long, long) + 203
8   libwx_osx_cocoau-2.9.dylib      0x00000001083761a7 wxStyledTextCtrl::CallTipShow(int, wxString const&) + 63
9   _stc.so                         0x000000010a07865f _wrap_StyledTextCtrl_CallTipShow + 415
10  org.python.python               0x00000001074f9fdc PyEval_EvalFrameEx + 14225
11  org.python.python               0x00000001074f6721 PyEval_EvalCodeEx + 1638
12  org.python.python               0x00000001074fcb13 fast_function + 282
13  org.python.python               0x00000001074f9919 PyEval_EvalFrameEx + 12494
14  org.python.python               0x00000001074f6721 PyEval_EvalCodeEx + 1638
15  org.python.python               0x000000010749dcaa function_call + 336
16  org.python.python               0x00000001074804fd PyObject_Call + 101
17  org.python.python               0x000000010748af2f instancemethod_call + 174
18  org.python.python               0x00000001074804fd PyObject_Call + 101
19  org.python.python               0x00000001074fc274 PyEval_CallObjectWithKeywords + 93
20  _core_.so                       0x0000000107b7b047 wxPyCallback::EventThunker(wxEvent&) + 455
21  libwx_osx_cocoau-2.9.dylib      0x0000000107e493b8 wxEvtHandler::ProcessEventIfMatchesId(wxEventTableEntryBase const&, wxEvtHandler*, wxEvent&) + 88
22  libwx_osx_cocoau-2.9.dylib      0x0000000107e49e1d wxEvtHandler::SearchDynamicEventTable(wxEvent&) + 85
23  libwx_osx_cocoau-2.9.dylib      0x0000000107e49d79 wxEvtHandler::TryHereOnly(wxEvent&) + 37
24  libwx_osx_cocoau-2.9.dylib      0x0000000107e49cc2 wxEvtHandler::ProcessEventLocally(wxEvent&) + 40
25  libwx_osx_cocoau-2.9.dylib      0x0000000107e49c54 wxEvtHandler::ProcessEvent(wxEvent&) + 88
26  libwx_osx_cocoau-2.9.dylib      0x000000010837c772 wxStyledTextCtrl::NotifyParent(SCNotification*) + 848
27  libwx_osx_cocoau-2.9.dylib      0x0000000108464959 Editor::NotifyDwelling(Point, bool) + 227
28  com.apple.CoreFoundation        0x00007fff96540804 __CFRUNLOOP_IS_CALLING_OUT_TO_A_TIMER_CALLBACK_FUNCTION__ + 20
29  com.apple.CoreFoundation        0x00007fff9654031d __CFRunLoopDoTimer + 557
30  com.apple.CoreFoundation        0x00007fff96525ad9 __CFRunLoopRun + 1529
31  com.apple.CoreFoundation        0x00007fff965250e2 CFRunLoopRunSpecific + 290
32  com.apple.HIToolbox             0x00007fff8d7b1eb4 RunCurrentEventLoopInMode + 209
33  com.apple.HIToolbox             0x00007fff8d7b1c52 ReceiveNextEventCommon + 356
34  com.apple.HIToolbox             0x00007fff8d7b1ae3 BlockUntilNextEventMatchingListInMode + 62
35  com.apple.AppKit                0x00007fff8c3dd533 _DPSNextEvent + 685
36  com.apple.AppKit                0x00007fff8c3dcdf2 -[NSApplication nextEventMatchingMask:untilDate:inMode:dequeue:] + 128
37  com.apple.AppKit                0x00007fff8c3d41a3 -[NSApplication run] + 517
38  libwx_osx_cocoau-2.9.dylib      0x0000000107f02b28 wxGUIEventLoop::OSXDoRun() + 106
39  libwx_osx_cocoau-2.9.dylib      0x0000000107e29b57 wxCFEventLoop::DoRun() + 39
40  libwx_osx_cocoau-2.9.dylib      0x0000000107d91b90 wxEventLoopBase::Run() + 88
41  libwx_osx_cocoau-2.9.dylib      0x0000000107d6a490 wxAppConsoleBase::MainLoop() + 88
42  _core_.so                       0x0000000107b76a44 wxPyApp::MainLoop() + 84
43  _core_.so                       0x0000000107bd94b7 _wrap_PyApp_MainLoop + 87
44  org.python.python               0x00000001074f9fdc PyEval_EvalFrameEx + 14225
45  org.python.python               0x00000001074f6721 PyEval_EvalCodeEx + 1638
46  org.python.python               0x000000010749dcaa function_call + 336
47  org.python.python               0x00000001074804fd PyObject_Call + 101
48  org.python.python               0x000000010748af2f instancemethod_call + 174
49  org.python.python               0x00000001074804fd PyObject_Call + 101
50  org.python.python               0x00000001074fa4f0 PyEval_EvalFrameEx + 15525
51  org.python.python               0x00000001074fcaaf fast_function + 182
52  org.python.python               0x00000001074f9919 PyEval_EvalFrameEx + 12494
53  org.python.python               0x00000001074f6721 PyEval_EvalCodeEx + 1638
54  org.python.python               0x00000001074f60b5 PyEval_EvalCode + 54
55  org.python.python               0x0000000107514eb8 run_mod + 53
56  org.python.python               0x0000000107514f5f PyRun_FileExFlags + 137
57  org.python.python               0x0000000107514aad PyRun_SimpleFileExFlags + 718
58  org.python.python               0x000000010752558b Py_Main + 3039
59  libdyld.dylib                   0x00007fff8ed8f7e1 start + 1

cut and paste broken on OS X

wx2.9

regions.py wx dependency

How hard is it to break the wx python dependency? I ask because I suspect the only way I'll ever be able to run simulation is in 64-bit. If the simulation is 64-bit but regions requires wx (32-bit), then the simulation can't run.

handlersubsystem needs refactoring

Remove "Spider" folder within handlers

Unable to run ConfigureSimulation or Simulate unless deleting the "Spider" directory

some bugs currently in dev

config files will be saved in src folder
prop mapping is not auto generated
got warning ([WARNING](/home/jim/LTLMoP/src/lib/hsubConfigObjects.py, line 357): No handler class found in file BasicSimInitHandler. Abort importing.)

The output format of fsa.stateToLTL is wrong

CURRENTLY:
def stateToLTL(state, use_next=False, include_env=True, swap_io=False):
""" swap_io is for the counterstrategy aut in mopsy """

def decorate_prop(prop, polarity):
    if int(polarity) == 0:
        prop = "!"+prop
    if use_next:
        prop = "next({})".format(prop)
    return prop

OUTPUT WILL BE : next(!prop) --> different from current .ltl output

SHOULD BE CORRECTED TO
def stateToLTL(state, use_next=False, include_env=True, swap_io=False):
""" swap_io is for the counterstrategy aut in mopsy """

def decorate_prop(prop, polarity):
    if use_next:
        prop = "next({})".format(prop)
    if int(polarity) == 0:
        prop = "!"+prop
    return prop

OUTPUT WILL BE: !next(prop)

No spaces allowed in robot's name?

It seems that spaces in a new robot's name result in bad behavior.

include original spec text as inline comments in LTL file

Handler Loading problem

When trying to simulate, the handlers associated with motion control, sensors and actuators are not loaded, resulting in the following error log:

[18:21:37] AttributeError
[18:21:37] :
[18:21:37] 'NoneType' object has no attribute 'name'

I attach a screenshot from the 'Configure Simulation' window:

Decomposition issue in grocery.regions

Cameron had to add the following hack to my specs in order to make the decomposition of "grocery.regions" work properly:

Group hack is between kitchen and table1, between entrance and table2

Issue with hideandseek.spec

Decomposing map into convex regions...
Creating LTL...
ERROR(8): Could not parse the sentence in line 31 because between is not recognized

ERROR(6): Could not parse the condition in line 31

ERROR: Aborting compilation due to syntax error.

Calibration tool freeze

Calibration tool freezes when the quit button is presses. This seems to not happen if the spec is saved before hitting quit.

Simulation Calibration Matrix

When using a simulated robot the option for the calibration matrix is grayed out and thus can not be modified. The issue this creates is that since the coordinates come from pixels the Y is actually flipped from what we would normally call the positive Y direction. Could this be fixed or could we get access to modify this matrix so we can put a -1 for the Y?

Simulated robot doesn't go anywhere

When I open the spec at:
https://github.com/LTLMoP/LTLMoP/blob/93ac8f2de5068506b56777aed1400271d8f2c960/src/examples/ltlworkshop/patrol.spec

When I simulate, the robot doesn't go anywhere, I just see this in the log:

[13:15:00] (Basic Simulator) Initializing Basic Simulator...
[13:15:00] (Basic Simulator) Start Basic Simulator...
[13:15:00] (SENS) Starting sensorHandler window and listen thread...
[13:15:01] (SENS) Starting actuatorHandler window...
[13:15:01] Loaded 96 states.
[13:15:01] Start!
[13:15:02] (ACT) Actuator extinguish is now 0!
[13:15:02] (ACT) Actuator radio is now 0!
[13:15:02] Currently pursuing goal #20 

Before, something like this was traced to convex decomposition being off, but I've turned that on. The only difference between this and the LTL spec in firefighting us turning bit encoding on. I've tried with convex decomposition on and off, and both seem to show this problem. I'm testing on Windows, in case it matters.

Configurations don't delete

Configurations will not be deleted when I click delete and ok on the GUI