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.
Eduardo Zambon
Interface (example)
None
Public
|
Date: 2009-01-14 10:51 Changed the usage message so that the CTL property is no longer shown as |
| 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 |