Skip to content
A Tabular Expression Toolbox
Branch: master
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.
tabster
README.md
Tabster - A Tabular Expression Toolbox REST API.ipynb

README.md

🚀 tabster

Tabster is an object oriented library used for verifying properties of tabular expressions such as completeness and disjointness through the use of SMT solvers. When a given property is not satisfied, Tabster returns counter examples to highlight the situation in which the property fails to hold.

Getting Started

Ensure the z3 SMT Solver is installed on your machine, see instructions here. To build the project, run a maven build using goals:"clean package assembly:single" - this should generate the ANTLR dependencies and generate the Tabster jar in the /target folder. Or download the latest stable version of the jar from the releases page.

Using the API

An excellent way to get started is to look at Tabster's unit tests.

Determining completeness of a tabular expression.

   @Test
	public void testSimpleCompleteTabularExpression() throws Exception {
		final ArrayList<SMTFunction> expressionVars = new ArrayList<SMTFunction>();
		final ArrayList<String> tabularExpression = new ArrayList<String>();
		tabularExpression.add("x > 0");
		tabularExpression.add("x < 0");
		tabularExpression.add("x = 0");   
		expressionVars.add(new SMTFunction("x", null, FunctionType.INT));
		final boolean isComplete = new TabularExpression(tabularExpression,expressionVars).checkCompleteness().satisfied();
		Assert.assertTrue(isComplete == true);
	}

Determining Disjointness of a tabular expression

@Test
	public void testSimpleNonDisjointTabularExpression() throws Exception {
		final ArrayList<SMTFunction> expressionVars = new ArrayList<SMTFunction>();
		final ArrayList<String> tabularExpression = new ArrayList<String>();
		tabularExpression.add("x > 5");
		tabularExpression.add("x < 5");
		tabularExpression.add("x < 8");   
		expressionVars.add(new SMTFunction("x", null, FunctionType.INT));
		PropertyVerificationResult result = new TabularExpression(tabularExpression,expressionVars).checkDisjointness(); 
		Assert.assertTrue(result.satisfied() == false);
		Assert.assertTrue(result.counterExamples().get(0).value().equals("0"));
	}
You can’t perform that action at this time.