Symbolic Executor for the High-Level Transformation Language TRON
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
README
lib
project
src
.gitignore
.sbtopts
LICENSE
README.md
SEMANTICS.md
SYNTAX.md
build.sbt

README.md

SymexTRON

GPLv3 licensed

A tool for symbolically executing TRON programs and generate white-box tests.

Prerequisites

  • Scala 2.11 (tested with 2.11.8)
  • SBT 0.13 (tested with 0.13.12)
  • Internet access for SBT to download dependencies

To run the native Plingeling solver, you must have the lib/solvers/‹platform› folder on your java.library.path (where ‹platform› should be replaced by either darwin (for OS X) or linux). This can be achieved by changing the setting in the repository included .sbtopts file. In case no native solver is available, it will fallback to the Java SAT4J solver which is compatible with more platforms but is slower.

To build:

First go to the source directory by using cd $HOME/Documents/SymexTRON and then call sbt compile.

To run tests:

Call sbt test in the SymexTRON directory.

To run the SLE paper evaluation:

Call sbt run in the SymexTRON directory.

The main evaluation source file is src/main/scala/examples/evaluation/Evaluation.scala, and it uses some of the example files from the containing examples folder.

The evaluation subjects from the paper and accompanying technical report can be found as follows:

Program File Object
RenameField Refactoring.scala RenameFieldRefactoring
RenameMethod Refactoring.scala RenameMethodRefactoring
ExtractSuper Refactoring.scala ExtractSuperclassRefactoring
ReplaceDelegation Refactoring.scala ReplaceDelegationWithInheritance
Fam2Pers ATLModelZooTransformation.scala FamiliesToPersonsTransformation
Path2Petri ATLModelZooTransformation.scala PathExp2PetriNetTransformation
Class2Rel ATLModelZooTransformation.scala ClassToRelationalTransformation
Toy1 IntListExample.scala IntListContainsElementExample
Toy2 IntListExample.scala IntListHeadTailEqExample
Toy3 Class2TableExample.scala Class2TableSimpleExample
Toy4 Class2TableExample.scala Class2TableDeepMatchingExample
Toy5 BlogPostFeedExample.scala BlogPostFeedTimestampsExample
Toy6 BlogPostFeedExample.scala BlogPostFeedCapitaliseTitlesExample
Toy7 ContactBookExample.scala ContactBookExample

To make an example program:

The description of the AST for type-definitions and programs is available in the SYNTAX.md file. The description of the heap representation is available in SEMANTICS.md file.

To make an example, start by creating a new file with your example name e.g. FooExample.scala which contains an object FooExample that inherits from the examples.Example trait. Then override the classDefs (containing the metamodel/type-definitions), pres (containing the initial memory) and prog (containing the TRON program) values to contain your desired program. Remember to add the following imports:

import semantics.domains._
import syntax.ast.Statement._
import syntax.ast._

For a simple example, see the IdIterExample in the examples package.

You can run an example by using sbt 'run-main ‹example name›', e.g. sbt 'run-main examples.IdIterExample' for running the tool on the IdIterExample.