We are thinking of implementing a few new features for Clafer. We opened a poll on the right, above the "Blog Archive". Please vote.
Here's a brief explanation of the features:
Allows for defining a clafer with the same name as the inherited one and restricting it's group cardinality, clafer cardinality, reference type, and bag to set. This is particularly useful for Example-Driven Modeling and specialization in architecture (e.g., Autosar uses it).
- module system
Allows for splitting a large model into smaller ones and also reusing common models. We are currently working on a simplest possible module system that will compile multiple files inside a single namespace.
- temporal constraints
Allow for specifying how model instances can evolve over time. In that view, the current Clafer constraints become simply global invariants. Using temporal constraints one can specify valid sequences of model instances. We're currenlty working on adding LTL constraints to Clafer and some more convenient syntactic sugar for behavior specification patterns and guarded and unguarded transitions.
- real numbers
Allow for reasoning on Real number arithmetic. We're planning on providing support in the ClaferSMT backend.
- string constraints
Allow for constraining the valid values of strings (using equality, prefix, postfix, maybe regexp) and operations on strings such as concatenation.
- inverse relation
Allows for conveniently specifying that two references are mutually inverse.
- transitive closure
Allows for specifying constraints over paths in recursive structures, such as, lists, trees and graphs.
Also, please post comments with other feature suggestions not on this list.