InequalitySystem: Don't require specifying the number of variables

The constructor of InequalitySystem no longer expects the number of variables in
the system and it is now possible to add inequalities with different number of
variables. All unspecified variables are assumed to have coefficient zero.

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SeparationUtility: Fix for previous changes in InequalitySystem

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
RegionUtility: Add & use getNumberOfEvents() helper function

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SeparationUtility: Change getFollowingState() into isEventEnabled()

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SeparationUtility: Require use of class instances

The idea of having a class with public static helper functions was originally
nice, but things are starting to get so complex that the number of arguments to
these helper functions becomes just too large.

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SeparationUtility: Optimize the k-bounded code

Instead of producing n*(n-1) many inequalities where n is the number of
(reachable) states in the LTS, this now "just" produces 2n inequalities. Still a
lot, but definitely better.

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SeparationUtility: Add debug output

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
InequalitySystem: Add a copy constructor

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SeparationUtility: Only set up a "basic" inequality system once

This changes the API for SeparationUtility once again. The constructor sets up
an inequality system for calculating regions and a member function is then used
for solving specific seperation problems.

This means that the generic set up is only done once and then re-used for later
problems.

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SeparationUtility: Safe code by calculating impure regions differently

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
InequalitySystem: Fix up outdated comments

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
InequalitySystem: Add comments to inequalities

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
InequalitySystemTest: Run solver-unspecific tests only once

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SeparationUtility: Add comments to inequalities

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SeparationUtility: Move member variables and constructor where they belong

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SeparationUtility: Add helper function for r_S(state)

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SeparationUtility: Simplify plain net & T-Net

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
RegionUtility: Fix a wrong method documentation

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SynthesizeModule: Remove outdated comment

Yes, this really is necessary and no, this is not a bug.

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>
SynthesizePN: Assert that the synthesized PN satisfies the specified properties

Signed-off-by: Uli Schlachter <uli.schlachter@informatik.uni-oldenburg.de>