coderocket / finefit Goto Github PK

Do not assume that the sut's driver class is in the finefit package.

currently we do not validate the content of the tables, this makes it difficult to correct mistakes because they appear as syntax errors at the Alloy file and it is difficult to correlate them with the location of the problem in the table.

Either ant or make or both

Currently when there's a syntax error we show the Alloy parser exception. It is difficult to map this error message back to the tabular spec.

currently it is only possible to determine the value of a state variable with an equation. However in some cases it is only possible to specify a constraint on the state variable. Borrowing an idea from Parnas we may use the syntax

x |

in the frame to indicate that the cells in the row for the variable x are not expressions but formulas. However it is not clear yet how to refer to the state variable in the formula.

currently we do not check that the model is internally consistent. That is, we do not check that the operations in the model maintain the invariant and that they are not trivial (their predicates are not 'false').

currently unless we explicitly set the values of all state variables in the retrieve function the values of these variables contain arbitrary (and therefore confusing) relations.

The readme file should explain how to build and run finefit, and what external dependencies it has.

Alloy does not provide 'true' and 'false' constants. But without 'true' it is cumbersome to define a total operation. In addition, it is cumbersome to specify that a relation is empty. Currently we have to do something like:

{ x : X, y : Y | y != y }

it would be better to define something like a function empty[X,Y]

When not providing the correct number of command line arguments print a usage message.

There are two problems here:

1. There is no way to specify the scope for integers (specifying them in the scope table fails because FineFit tries to generate a signature for Int)
2. The current way in which we generate the scope definition does not work with Ints for some reason.

Currently we only support input variables for the tabular notation. We should add support for output variables.

Currently we ignore the scope size provided in the spec.

currently we have to write the full name of the exception class in the exception table.

This is a utility function that should not be coded by each and every sut implementor