verivital / hyst

HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models
http://verivital.com/hyst/
Other
15 stars 18 forks source link

order reduction pass #13

Closed ttj closed 8 years ago

ttj commented 8 years ago

This mostly works, I'm in part going to do the pull request now as we're getting very fragmented with the branches even with upstream pulls, and I think I just broke something upstream and want to get it fixed sooner rather than later. Next fork to try to merge will be xspeed, followed by stan's lut

Missing parts: there is a parser bug for large models, particularly with large initial conditions, I'm not sure if this will get resolved anyway with Stan's parser changes, so I'm ignoring it for now. I commented the large order reduction test for now and all tests passed on my system.

Other changes:

stanleybak commented 8 years ago

There seems to be test code in the mode order reduction pass code: proxy.eval("disp('hello world'); disp('test123'); clock");

There are many commented-out annotations in StateflowSpPrinter which should be deleted: //@Nullable

StateflowSpPrinter has commented-out test code that should be deleted:

//Display 'hello world' just like when using the demo
//proxy.eval("disp('hello world'); disp('test123'); clock");
//proxy.eval("disp('" + originalFilename + "'); disp('test123'); clock");

There are other cases in StateflowSpPrinter.java where there is code commented out that will never be re-added. This code should be deleted. If you do end up reverting, the code will be saved in git somewhere as an old version. For the master branch we shouldn't have such code.

I saw a timeout was added to the unit tests. Unit tests should be quick. We probably want to remove any unit tests that take a long time. They might be okay as regression tests, but generally those are for when bugs are found. Is there something the longer test tries that a shorter test can't do?

Running the unit tests without matlab fails:

 [junit] matlabcontrol.MatlabConnectionException: Could not launch MATLAB. This is likely caused by MATLAB not being in a known location or on a known path. MATLAB's location can be explicitly provided by using matlabcontrol.MatlabProxyFactoryOptions.Builder's setMatlabLocation(...) method.
...
[junit]     at matlabcontrol.RemoteMatlabProxyFactory.createProcess(RemoteMatlabProxyFactory.java:323)
    [junit]     at matlabcontrol.RemoteMatlabProxyFactory.requestProxy(RemoteMatlabProxyFactory.java:125)
    [junit]     at matlabcontrol.RemoteMatlabProxyFactory.getProxy(RemoteMatlabProxyFactory.java:144)
    [junit]     at matlabcontrol.MatlabProxyFactory.getProxy(MatlabProxyFactory.java:81)
    [junit]     at com.verivital.hyst.passes.complex.OrderReductionPass.runPass(Unknown Source)
    [junit]     at com.verivital.hyst.passes.TransformationPass.runVanillaPass(TransformationPass.java:61)
ttj commented 8 years ago

It seems replying via email didn't add comments here, will try to put everything here next time. Here's the discussion so far:

Stan:

Yeah our terminology for the tests is a bit imprecise. Usually the distinction is between functional tests (end-to-end) and unit tests (subcomponent or submodule). There is another distinction between regression tests (which detect behavior that breaks when a new feature is added) and validation or features tests (which detect that the new behavior works as expected, for example in test-first development).

Generally the regression tests were made as end-to-end functional tests which run Hyst to completion and even run each tool on each generated model (with a timeout). The unit tests were meant to be tests of specific methods, or a specific pass on a toy model, although the printer tests go against this somewhat.

What are your thoughts on the test organization?

Taylor: Luan added (1) tests for order reduction (requires calling matlab and may be slow) and (2) tests for the SLSF converter, which also requires calling Matlab and may be slow. So, these encompass printer tests as well as general tests. Probably Luan could create some subfunction unit tests for the order reduction pass (e.g., matrix conversion to/from Matlab) in addition to the full tests he already has in there.

Perhaps we should add a third category of tests that may be slow with such timeouts? Maybe call these validation/feature tests (but whatever is fine for me)?

My use case is that I typically just run the test thing that executes the unit+regression tests, and I'd probably do so for these. After first launch they're relatively quick.

Also, Stan, this is another example of where we need to detect if tools are installed. Could you please point Luan to whereever this was set up for Python / Python toolboxes, as different tests should be run/skipped based on the configuration of the host system? There are also several granularities of functionality here: (1) is matlab installed? then (2) is stateflow installed (plus possibly some other toolboxes, but that's the main one)?

This goes beyond tests of course, so it would be good to have such a configuration management set up to detect what features are possible/not (maybe a cleaner way to handle the Z3 stuff as well...).

Luan: I think whenever we call matlab from Hyst ( for both order reduction and stateflow converter ), we may get the timeout problem in the first launch. I can generate some sub-function tests for the order reduction, but I am not sure it will solve a problem here. Moreover, for the stateflow converter, we need a long test to make sure the translation can work properly. I agree that adding another testing category will be the good way to go. If you want me to do that, please guide me since I am not familiar with the current set up for Python.

Also I just removed commented-out annotations and test codes in the StateflowSpPrinter and the order reduction pass.

ttj commented 8 years ago

Ok, that's all I have time for now, please (a) Luan go through the list of remaining changes to make sure you've addressed everything in some way, and (b) check it out Stan and let us know of any new major issues.

ttj commented 8 years ago

Stan: can we go ahead and merge this?

stanleybak commented 8 years ago

The code changes look alright. I still have an error when running the unit tests, which should be resolved before merging.

   [junit] matlabcontrol.MatlabConnectionException: Could not launch MATLAB. This is likely caused by MATLAB not being in a known location or on a known path. MATLAB's location can be explicitly provided by using matlabcontrol.MatlabProxyFactoryOptions.Builder's setMatlabLocation(...) method.
    [junit] OS: Linux
    [junit] Command: [matlab, -desktop, -r, javaaddpath '/home/stan/repositories/hyst/lib/matlabcontrol-4.1.0.jar'; matlabcontrol.MatlabClassLoaderHelper.configureClassLoading(); javarmpath '/home/stan/repositories/hyst/lib/matlabcontrol-4.1.0.jar'; matlabcontrol.MatlabConnector.connectFromMatlab('PROXY_RECEIVER_e078a77f-d785-475f-9119-2e3dfca175db', 2100);]
    [junit] Environment: {PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/usr/lib/jvm/java-8-oracle/bin:/usr/lib/jvm/java-8-oracle/db/bin:/usr/lib/jvm/java-8-oracle/jre/bin, XAUTHORITY=/home/stan/.Xauthority, XMODIFIERS=@im=ibus, XDG_DATA_DIRS=/usr/share/ubuntu:/usr/share/gnome:/usr/local/share/:/usr/share/, GDMSESSION=ubuntu, MANDATORY_PATH=/usr/share/gconf/ubuntu.mandatory.path, TEXTDOMAINDIR=/usr/share/locale/, GTK_IM_MODULE=ibus, DBUS_SESSION_BUS_ADDRESS=unix:abstract=/tmp/dbus-imauGTUyuV, DEFAULTS_PATH=/usr/share/gconf/ubuntu.default.path, XDG_CURRENT_DESKTOP=Unity, COLORTERM=gnome-terminal, UPSTART_SESSION=unix:abstract=/com/ubuntu/upstart-session/1000/1947, QT4_IM_MODULE=xim, SESSION_MANAGER=local/stan-thinkpad-t550:@/tmp/.ICE-unix/2097,unix/stan-thinkpad-t550:/tmp/.ICE-unix/2097, LOGNAME=stan, JOB=dbus, PWD=/home/stan/Desktop/repositories/hyst/src, DERBY_HOME=/usr/lib/jvm/java-8-oracle/db, IM_CONFIG_PHASE=1, LANGUAGE=en_US, PYTHONPATH=:/home/stan/repositories/hyst/src/hybridpy, WINDOWID=81788939, FLOWSTAR_BIN=/home/stan/tools/flowstar-1.2.3/flowstar, SHELL=/bin/bash, LESSOPEN=| /usr/bin/lesspipe %s, INSTANCE=, OLDPWD=/home/stan/Desktop/repositories/hyst, GNOME_DESKTOP_SESSION_ID=this-is-deprecated, GTK_MODULES=overlay-scrollbar:unity-gtk-module, J2REDIR=/usr/lib/jvm/java-8-oracle/jre, CLUTTER_IM_MODULE=xim, XDG_SESSION_PATH=/org/freedesktop/DisplayManager/Session0, TEXTDOMAIN=im-config, COMPIZ_BIN_PATH=/usr/bin/, SESSIONTYPE=gnome-session, DREACH_BIN=/home/stan/tools/dreach/dReal-2.15.01-linux/bin/dReach, LS_COLORS=rs=0:di=01;34:ln=01;36:mh=00:pi=40;33:so=01;35:do=01;35:bd=40;33;01:cd=40;33;01:or=40;31;01:su=37;41:sg=30;43:ca=30;41:tw=30;42:ow=34;42:st=37;44:ex=01;32:*.tar=01;31:*.tgz=01;31:*.arj=01;31:*.taz=01;31:*.lzh=01;31:*.lzma=01;31:*.tlz=01;31:*.txz=01;31:*.zip=01;31:*.z=01;31:*.Z=01;31:*.dz=01;31:*.gz=01;31:*.lz=01;31:*.xz=01;31:*.bz2=01;31:*.bz=01;31:*.tbz=01;31:*.tbz2=01;31:*.tz=01;31:*.deb=01;31:*.rpm=01;31:*.jar=01;31:*.war=01;31:*.ear=01;31:*.sar=01;31:*.rar=01;31:*.ace=01;31:*.zoo=01;31:*.cpio=01;31:*.7z=01;31:*.rz=01;31:*.jpg=01;35:*.jpeg=01;35:*.gif=01;35:*.bmp=01;35:*.pbm=01;35:*.pgm=01;35:*.ppm=01;35:*.tga=01;35:*.xbm=01;35:*.xpm=01;35:*.tif=01;35:*.tiff=01;35:*.png=01;35:*.svg=01;35:*.svgz=01;35:*.mng=01;35:*.pcx=01;35:*.mov=01;35:*.mpg=01;35:*.mpeg=01;35:*.m2v=01;35:*.mkv=01;35:*.webm=01;35:*.ogm=01;35:*.mp4=01;35:*.m4v=01;35:*.mp4v=01;35:*.vob=01;35:*.qt=01;35:*.nuv=01;35:*.wmv=01;35:*.asf=01;35:*.rm=01;35:*.rmvb=01;35:*.flc=01;35:*.avi=01;35:*.fli=01;35:*.flv=01;35:*.gl=01;35:*.dl=01;35:*.xcf=01;35:*.xwd=01;35:*.yuv=01;35:*.cgm=01;35:*.emf=01;35:*.axv=01;35:*.anx=01;35:*.ogv=01;35:*.ogx=01;35:*.aac=00;36:*.au=00;36:*.flac=00;36:*.mid=00;36:*.midi=00;36:*.mka=00;36:*.mp3=00;36:*.mpc=00;36:*.ogg=00;36:*.ra=00;36:*.wav=00;36:*.axa=00;36:*.oga=00;36:*.spx=00;36:*.xspf=00;36:, SHLVL=1, LESSCLOSE=/usr/bin/lesspipe %s %s, COMPIZ_CONFIG_PROFILE=ubuntu, QT_IM_MODULE=ibus, JAVA_HOME=/usr/lib/jvm/java-8-oracle, TERM=xterm, XFILESEARCHPATH=/usr/dt/app-defaults/%L/Dt, XDG_CONFIG_DIRS=/etc/xdg/xdg-ubuntu:/usr/share/upstart/xdg:/etc/xdg, LANG=en_US.UTF-8, GNOME_KEYRING_CONTROL=/run/user/1000/keyring-PRghyk, XDG_SEAT_PATH=/org/freedesktop/DisplayManager/Seat0, XDG_SESSION_ID=c2, SELINUX_INIT=YES, DISPLAY=:0, _=/usr/bin/ant, GDM_LANG=en_US, XDG_GREETER_DATA_DIR=/var/lib/lightdm-data/stan, GPG_AGENT_INFO=/run/user/1000/keyring-PRghyk/gpg:0:1, DESKTOP_SESSION=ubuntu, SESSION=ubuntu, USER=stan, CLASSPATH=.:/usr/local/lib/antlr-4.5-complete.jar:, XDG_MENU_PREFIX=gnome-, VTE_VERSION=3409, SSH_AUTH_SOCK=/run/user/1000/keyring-PRghyk/ssh, XDG_SEAT=seat0, NLSPATH=/usr/dt/lib/nls/msg/%L/%N.cat, QT_QPA_PLATFORMTHEME=appmenu-qt5, SPACEEX_BIN=/home/stan/tools/spaceex/spaceex, XDG_VTNR=7, XDG_RUNTIME_DIR=/run/user/1000, HOME=/home/stan, GNOME_KEYRING_PID=1934}
    [junit]     at matlabcontrol.RemoteMatlabProxyFactory.createProcess(RemoteMatlabProxyFactory.java:323)
    [junit]     at matlabcontrol.RemoteMatlabProxyFactory.requestProxy(RemoteMatlabProxyFactory.java:125)
    [junit]     at matlabcontrol.RemoteMatlabProxyFactory.getProxy(RemoteMatlabProxyFactory.java:144)
    [junit]     at matlabcontrol.MatlabProxyFactory.getProxy(MatlabProxyFactory.java:81)
    [junit]     at com.verivital.hyst.passes.complex.OrderReductionPass.runPass(Unknown Source)

For the python calls inside Hyst, I use a singleton object defined in PythonBridge.java. This means that the constructor is private to PythonBridge, and you can only get an instance of the object using getInstance(), which guarantees only a single process will be created. The process is created by looking for the executables python2.7 or python in the paths defined in the environment variable HYST_PYTHON_PATH as well as the standard PATH environment variable, so that if multiple versions of python are installed in the machine, the specific one can be chosen by setting HYST_PYTHON_PATH.

If the python executable, or any of the required python libraries (currently sympy and scipy) are not present, then an AutomatonExportException is raised in getInstance(). The user can check if python is present by calling hasPython() which tracks if the process is open and catches the exception if it fails to open a process. I also added an java shutdown hook upon opening the process, so the python process is closed whenever java shuts down.

The unit tests which require python bridge, for example testing the hybridization pass, first call hasPython(), and only proceed if python is present, otherwise doing nothing (so the tests always pass, even if python is not present or misconfigured).

For Matlab, a similar strategy could be taken, for example creating a singleton MatlabBridge object to ensure that a Matlab process is only created once, even if it's used by multiple passes or printers (I'm not sure what the default behavior of the MatlabProxyFactory is). You could then have a hasMatlab() method that gets called before any test that uses Matlab, in order to ensure that the doesn't doesn't fail. I'm not sure this is the approach you want to take, though.

In my opinion, at least initially, I don't think there's too much that can be gained by having more fine-grained support for individual features (matlab and stateflow versus just matlab), versus the amount of effort it would take to support it. It's much easier to tell someone that for the model order reduction pass they should meet our matlab dependencies, which include matlab, stateflow, and any toolkits we require. Alternatively, you could check, in code, for individual matlab toolkits and set a series of flags that are accessible in Hyst. For any tests that use that feature, you would then call the appropriate method (for example, hasMatlabStateflow()).

I didn't add long tests for python, since the process opens in, at worst, a few seconds. I run the unit tests often, and the regression tests only when merging. It might be good to put short tests as unit tests, and long tests as regression tests (maybe rename regression tests to long tests or something?). The regression tests are just a python script; if you want to add something to them that runs passes and such, I think it can just be added at the bottom of the main function.

ttj commented 8 years ago

I tried to add some stuff for something like a MatlabBridge, this caused a variety of problems (particularly performance bugs) related to relaunching matlab I don't have time to fully fix now, but I got it roughly working. There was still some issue in how to detect if Matlab is there or not I think, so please check if the tests are okay now, as I cannot fully test this on my setup.

stanleybak commented 8 years ago

ok, tests seem to pass for me so I think we can merge now.

ttj commented 8 years ago

ok, great, going to merge. I will work to clean up the matlab interface more later on.

Following this merge, we will look to merge Rajarshi's xspeed printer, then Stan's latest lookup table additions.

Luan and Christian: please make sure you can still run everything (pull from mainline / do an upstream sync/merge), as I only tested this on my set up, and Stan did not run it seems (the tests were bypassed without matlab, similar to how the python tests are bypassed if packages/python are not detected).