Summary of PSYCO Extension and Evaluation

Introduction

PSYCO is a tool for generating interfaces of components using automata learning. Currently the learning algorithm is not able to decide termination during the learning process and executes until it hits a predefined limit or runs out of a timing budget. My GSOC project aims on extending PSYCO by a breadth-first search, to determine a termination criterion for the learning algorithm.

According to my proposal, I implemented a breadth-first search within the PSYCO environment. As Z3 performance was sufficient for our needs we decided against implementing any Ordered Binary Decision Diagramm approaches. I further had a look on using Z3s quantifier elimination engine, but it turns out, that Z3 is more efficient on solving quantified formulas then eliminating quantifiers. Therefore we have not followed this direction further.

Instead we decided to merge back and debug some old ideas of Falk Howar, Dimitra Giannakopoulou, and Jorge Navas using interpolation to speed up PSYCOs interface learning and overall run time. This allows to explore interfaces up to depths determined by the symbolic search in reasonable times.

Apart from implementing the search algorithm and merge it back to the official PSYCO repository, we summed up our results gained from the search as a submission for the Java Path Finder workshop 2016.

Work packages

During my Google Summer of Code project I implemented a breadth-first search to extend PSYCOs capabilities. This includes the following issues:

• Implement an Enumerative Search to explore finite search spaces, without method parameters within the transition system.
• Implement a Symbolic Search to explore finite search spaces. Method parameters are allowed this time in the transition system.
• Created a connection to Z3 quantifier elimination algorithm and decided, that it should not be used in the search.
• Refactoring the CEV example for evaluation purpose.
• Enhancement to save a transition system as a file.
• Define a storage file format for a transition system.
• Load a transition system from a file, instead of using jDart to generate transition paths prior to the search run.
• Enhancement to write out search and model learning results into files for later use.
• Optimizations:
• • Errors can only be reached once
• • Stutter Transitions are ignored
• • Constant assignment cuts path history
• • In-place state history shortening state descriptions
• • Refactored architecture to share as match code as possible between symbolic and enumerative search version. This also forms a kook-up point for future extensions.

Overall this covers the content of my project proposal.

The work is mainly merged back to the official PSYCO github repository.

Commits to the PSYCO repository

But small parts are in the jConstraints and jConstraints-z3 repository:

Commits to the jConstraints repository

Commits to the jConstraints-z3 repository

For project documentation, please have a look on my project wiki.

I want to point out to the algorithm description page as this is the most detailed description of the work done beside the source code.

Apart from the search implementation I merged older changes from Falk Howar, Dimitra Giannakopoulou, and Jorge Navas to the PSYCO repository. This comprises mainly the gov.nasa.jpf.psyco.interpolation package. I adopted it to fit in the current PSYCO framework, but the theoretical work and main part of the implementation is done by Falk Howar before the project started.

The merge maintained the original history, so contribution can be tracked backed to the author. Apart from merging interpolation capability, I also used some time of my Google Summer of Code project, to fix bugs in the term parser of jConstraints-smtinterpol. (See commits to the jConstraints-smtinterpol repository)

Installation and Usage

I suggest to use PSYCO by powering up a vagrant virtual machine, as all dependency are predefined. A Vagrant file is provided in the PSYCO repository. Otherwise you will need the following JPF modules apart from PSYCO:

• JPF-core
• JPF-jDart
• jConstraints
• jConstraints-z3
• jConstraints-smtinterpol

Once correctly installed you should be able to any of the included example. So for running the net example included, execute:

#!bash
path/To/jpf-core/bin/jpf src/examples/issta/net/search.jpf

Expected results for the examples are also provided.

Open Points

There are still a few bugs in the connection between jConstraints and the smtinterpol solver. We are planing to fix them within the next weeks.

Bug 1

So running the math examples, fails currently, because bitvector casts are not supported:

java.lang.IllegalStateException: Cannot handle cast bitvector expressions at gov.nasa.jpf.constraints.solvers.smtinterpol.SMTInterpolExpressionGen erator.visit(SMTInterpolExpressionGenerator.java:217) at gov.nasa.jpf.constraints.solvers.smtinterpol.SMTInterpolExpressionGen erator.visit(SMTInterpolExpressionGenerator.java:49) at gov.nasa.jpf.constraints.expressions.BitvectorExpression.accept(Bitve ctorExpression.java:92) at gov.nasa.jpf.constraints.expressions.AbstractExpressionVisitor.visit( AbstractExpressionVisitor.java:123) at gov.nasa.jpf.constraints.solvers.smtinterpol.SMTInterpolExpressionGen erator.visit(SMTInterpolExpressionGenerator.java:111)

Run interpolation psyco on issta2013/math/learn.jpf to reproduce trace.

Bug 2

Running the AlternateBit example leads to the following error, which seems connected to the modulo-operator:

Exception in thread "main" de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Undeclared function symbol (% Int Int) at de.uni_freiburg.informatik.ultimate.logic.NoopScript.term(NoopScript.java:286) at de.uni_freiburg.informatik.ultimate.logic.NoopScript.term(NoopScript.java:262) at gov.nasa.jpf.constraints.solvers.smtinterpol.SMTInterpolExpressionGenerator.visit(SMTInterpolExpressionGenerator.java:163) at gov.nasa.jpf.constraints.solvers.smtinterpol.SMTInterpolExpressionGenerator.visit(SMTInterpolExpressionGenerator.java:49) at gov.nasa.jpf.constraints.expressions.NumericCompound.accept(NumericCompound.java:142)

Bug 3

The Accelerometer example does not run in the interpolation branch, caused by the division operator:

Exception in thread "main" de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Undeclared f unction symbol (/ Int Int) at de.uni_freiburg.informatik.ultimate.logic.NoopScript.term(NoopScript.java:286) at de.uni_freiburg.informatik.ultimate.logic.NoopScript.term(NoopScript.java:262) at gov.nasa.jpf.constraints.solvers.smtinterpol.SMTInterpolExpressionGenerator.visit(SMTIn terpolExpressionGenerator.java:161) at gov.nasa.jpf.constraints.solvers.smtinterpol.SMTInterpolExpressionGenerator.visit(SMTIn terpolExpressionGenerator.java:49) at gov.nasa.jpf.constraints.expressions.NumericCompound.accept(NumericCompound.java:142)

##Future Project Ideas## Next, to continue this project, we will combine PSYCOs interface generation tighter with the search. Up to know they are independent components. We currently plane to use the search as counter example generator. So the idea is to unroll the internal state system for a component and at the same time the generated interface. If a mismatch occurs between the internal and the external visible behavior, for example the search runs into an error but not the interface, an counterexample is found. We are planing to improve PSYCOs learned interface quality by this and also speed up the interface learning phase using the search instead of the current equivalence test.

The search itself is still in a beta version, but it behaves stable at the moment.