mantkiew Release 0.5.0 (#94)
23c7b41 Feb 1, 2018
Release 0.5.0 (#94)
* Behavioral (#56)

* 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

* prepare 0.5.0 release and travis build

* add upperbound on base dependency

* allow happy 1.19.5 again as 1.19.8 is not available in hvr's PPA

* allow alex 3.1.7 again as it is the latest available in hvr's PPA

* remove unnecessary version constraint on clafer library
23c7b41