Share

Groove

Tracker: Bugs

5 ModelChecker requires two command line arguments - ID: 1941059
Last Update: Settings changed ( zambon )

In contrast to the printed usage message and the user manual, the
ModelChecker of GROOVE 3.0.0 requires a grammar-location and a property.
The usage message and the property say the property is optional.

The erroneous code is at least in
groove.verify.CTLModelChecker.processArguments(), because if argList.size()
!= 2, the error message I receive is printed:
Error: You should at least provide the location of the graph production
system to be verified.


Christoph Schwering ( schwering ) - 2008-04-12 20:59

5

Closed

Fixed

Eduardo Zambon

Interface (example)

None

Public


Comment ( 1 )

Date: 2009-01-14 10:51
Sender: zambon

Changed the usage message so that the CTL property is no longer shown as
optional.




Attached File

No Files Currently Attached

Changes ( 5 )

Field Old Value Date By
resolution_id None 2009-08-18 07:33 zambon
status_id Open 2009-01-14 10:51 zambon
allow_comments 1 2009-01-14 10:51 zambon
close_date - 2009-01-14 10:51 zambon
assigned_to nobody 2009-01-14 08:51 rensink