Release 0.5.0 #94
Merged
Release 0.5.0 #94
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* Added temporal language elements to grammar * Integrated behavioral clafer grammar and implemented desugaring of temporal expressions, transitions and modalities. * Adjusted grammar; Finished implemented desugaring rules; Fixed sugaring of some expressions; Added simple test runner 'desugartests.sh' in test/positive/ * Implemented Alloy-Ltl model code generator * Refreshed grammar generated code and added missing files to clafer.cabal * AlloyLtl generator: fixed mutable clafer cardinalities * Improvments in AlloyLtl generator: created root clafer which is umbrella for all top level clafer relations. Changed time binding in constraints. * Updated gramamr with new pattern expressions and updated pattern ltl encodings * removed duplicate clafer names from test cases * ClaferBinding = Maybe UID Pass GenEnv instead of ClaferArgs around removed ClaferArgs from GenCtx * change soft constraint from `(...)` to `assert [...]` * Added lonce temporal pattern * Fixed parent constraint; fixed first local time instance declaration; fixed group cardinality constraint * inheritance of mutability * regen parser * fixed syntax of transitions/removed async transition --> next step (X) -->> many steps (U) * removed FinalConstraint, added IClaferModifiers and their inheritance, html rendering of temp modifiers, root clafer initial and final, * fixed warnings * fixed test cases using set intersection (& to **) * fixed changing & to ** * initial and final inherited correctly (were "flipped") * added the missing rules to HTML generator (fixed non-exhaustive patterns) * html rendering of transition on clafer decl and the remaining patterns * moved PowerWindow models to experimental they use redefinition, which is not supported yet * fixed "before" pattern was "between" by mistake * updated all tmp positive test cases, moved history to experimental removed redundant test cases (clones) * updated regressions for xml, html, and dot * updated regressions for alloy and js * fixed test case (broken comment) * added temporal keywords to reserved keyword list * automatic selection of static of dynamic Clafer subset for Alloy generation. Choco and Python outputs only for static subset. * fixed test suites for default Alloy42 mode * updated Python regressions and few others * removed validation is NoCompilerResult, fixed XML Schema * updated XML validator * bumped version to 0.4.0 * fixed description in readme * Fixed: root level constraint issues, mutable subclafer cardinality facts, restricted network package version in clafer.cabal * Allow using AlloyLtl for static subset of Clafer Must provide two modes: 4.1 or 4.2 + whether LTL or not (default) * code formatting and error msgs * fixed Int generation need to check istop otherwise we get @r_integer instead of Int generated * update regression * Updated to work with the new version of custom BNFC tool * updated missed old Absclafer import * create correct root in UID->IClafer map, * scope computation: multiply by trace length for mutable clafers renamed `fixed_scope` to `trace_len` * Fixed issue #1: after-until scope was not properly parsed * Fixed translation of WeakUntil operator in AlloyLtl ouput * added assertion generation to AlloyLtl * Fixed assertions in AlloyLtl * adapted the new python generator to behavioral * ported group card. fix to AlloyLtl -- TODO: need to include time stamps genParentSubrelationConstriant (needed for proper inheritance from nested abstract clafers) * fixed --trace-len default to 10 * preliminary fix for quantifier expression in form `all x : A.B.C | x...`. Added test cases. however, for the resulting Alloy code, Alloy complains that "Analysis cannot be performed since it requires higher-order quantification that could not be skolemized." * moved redefinition test case to failing it is not implemented yet * Fixed desugaring of lonce pattern with before scope * added a missing assertion to tmp_clafertransitions02.cfr * Added parenting constraint that prevents subgraphs which are not connected to root * updated test cases * updated test case for eventually constraint * updated test case and commented constraint giving error * testcase for history constraint * TrafficLight Update * test for commit * added to regression testing * AlloyLtl changes: Added local_first function and switched constraints to using it; Added several constraints to prevent subinstances from reappearing and changing parents during a trace. * Fixed parenting constraint in alloyltl generator * fixed Suite.Positive * Deferred initally desugaring until after analysis (generator stage), which fixed alloy output of initially constraint * rebuilt XsdCheck * fix build on GHC 7.10.1, remove warnings * Fixed bFoldlOr to have a more canonical name and implementation This is mostly to test my build, test and Haskell setup + commit rights * refactored the header of the AlloyLtl generator Tried to make both the generator and the alloy output more readable. Primarily wanted to get into the code a bit. * Updated Alloy Ltl encodings to the latest proposal by A.Cunha * Partially fixed transitions issue #9. Alloy output now compiles, but needs extra fining * Resolved issue when reference to mutable parent was not joined with correct t relation (it was getting t primes although it needed t) * Partly fixed issue #3: local variable declarations are now allowed - there is still issue with declarations in top level constraints. Also fixed parenting constraints, that prevent clafers having subclafers if they have no parents. * Removed leftover trace call * Removed unnecessary domain restrictions on State and replaced declaration 'one t:' to 'let t=' * Added empty function root clafer adjustment * Added finaltarget and finalref modifiers for references. Desugaring needs more work. * Fix desugaring of reference expressions with modifiers * Move inline state declarations to outside file to be embedded using template haskell * Remove _mutable field from IClafer; Use final modifier instead to detect mutability * Remove debugging trace printing from Inheritance Resolver * Add state suffix to mutable reference clafers * Generate top level clafer ids without 'r_' relation prefix * Remove leftover debugging traces * Fix alloyltl encoding of initial modifier * remove Python mode and skip-goals option, remove .x and .y files, upgrade to LTS-5.15 * fixed test cases. "X" is a keyword in bClafer * GHC version compatibility for ErrM.hs * fixed grammar for min, max, and if/then/else. Fixed a test case 'X' is reserved All test suite models now compile * updated test case 'objectivesMinMax' - 'X' is a reserved keyword * Ensure that instance occurs at least once as child of parent instance * only produce Choco output for static subset * add test cases * fixed test/experimental/tmp_PowerWindowDesignModel.cfr * commented out or removed failing temporal assertions * added temporal regressions for reference * fix to be , and to be * warning cleanup, missing pattern matches, linting * updated regressions * styling of temporal keywords, updated regressions * compile temporal models to .tmp.als, and static models to .als so that ClaferIG can distinguish * save .tmp.als files as .als for backwards compatibility * Release 0.5.0 * add stateTrace.als to datafiles so that it's present in sdist. Otherwise cabal install does not work
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Add behavioral clafer.