FiniteSatUSE Files

FiniteSatUSE (USE) is implemented in Java. In order to run the  tool, enter the following command  at the prompt (assuming the current working 
directory is the directory of the FiniteSatUSE.jar file).

java -jar FinteSatUSE.jar

Now you are asked to enter a USE file path (a text file). You have the option to exit by typing "end"
Examples for USE files appear in https://goo.gl/zVvHNz

The possible commands

-P               Propagate the disjoint constraints within the class hierarchy cycles .
-save <file name>Save the modified model (should be used only with -P flag raised).
-S               Show the model.
-D               Detect finite satisfiability problems.
-I               Identify cause of finite satisfiability problems (critical cycles).
-C               Identify class hierarchy cycles with disjoint or complete constraints
-Sim             Simplification


*****************************************************************************************************

Examples:
Below we show the application of the simplification method. This is example 1 from https://goo.gl/ncSMxS. For more examples, follow the link.

Example 1 (The class diagram appears in https://goo.gl/ncSMxS)

	model paperRedundancy2013
	class A
	end
	class B
	end
	class C
	end
	association r1 between
	A[2..6] role p1
	B[4..8] role p2
	end
	association r2 between
	B[1..3] role p3
	C[2..4] role p4
	end
	association r3 between
	C[2..4] role p6
	A[9..*] role p5
	end
	association q between
	A[1..6] role q1
	B[2..10] role q2
	end



Running FiniteSatUSE:


>java -jar FiniteSatUSE.jar

 FiniteSatUSE 2011-2018 Ben-Gurion University of the Negev
===========================================================

Please enter a USE file path to examine or type end to exit:
C:\Tests\Redundancy\test.use

Please enter one of the following commands:
--------------------------------------------------------------------------
-P               Propagate the disjoint constraints within the class
                 hierarchy cycles .
-save <file name>Save the modified model (should be used only with -P 
                 flag raised).
-S               Show the model. 
-D               Detect finite satisfiability problems.
-I               Identify cause of finite satisfiability problems 
                 (critical cycles).
-C               Identify class hierarchy cycles with disjoint or 
                 complete constraints 
-Sim             Simplification 
-----------------------------------------------------------------------------
-Sim -S -save C:\Tests\Redundancy\testTightened.use
Simplification:
There is a redundancy problem in this model.
Redundancy problem with associations: 
 r3 r2 r1 
 and classes: 
 a c b

Would you like to tighten this model(y/n)?

y
There is no redundancy problems in this model.

The Model:
model paperRedundancy2013

class A
attributes
end

class B
attributes
end

class C
attributes
end

association q
between
 A[1..6] role q1
 B[2..10] role q2
end

association r1
between
 A[6] role p1
 B[4] role p2
end

association r2
between
 B[3] role p3
 C[2] role p4
end

association r3
between
 C[4] role p6
 A[9] role p5
end

The file has been saved

---------------------------------------------------------------------------------
Overall execution time: 1984 ms.
---------------------------------------------------------------------------------