call-alloy 0.5 → 0.5.0.1
raw patch · 4 files changed
+168/−1 lines, 4 filesdep ~basedep ~extradep ~filepathPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: base, extra, filepath
API changes (from Hackage documentation)
- Language.Alloy.Call: getIdentityAs :: forall m b (a :: Type -> Type). MonadThrow m => String -> (String -> Int -> m b) -> Entry Map a -> m b
+ Language.Alloy.Call: getIdentityAs :: MonadThrow m => String -> (String -> Int -> m b) -> Entry Map a -> m b
- Language.Alloy.Call: type Entries (a :: Type -> Type -> Type) = a Signature Entry a Set
+ Language.Alloy.Call: type Entries a = a Signature (Entry a Set)
- Language.Alloy.Exceptions: [CallAlloyException] :: forall e. Exception e => e -> CallAlloyException
+ Language.Alloy.Exceptions: [CallAlloyException] :: Exception e => e -> CallAlloyException
Files
- call-alloy.cabal +4/−1
- test/unit/readmeExampleInstance.hs +137/−0
- test/unit/readmeExampleResult.hs +7/−0
- test/unit/readmeExampleSpecification.als +20/−0
call-alloy.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: call-alloy-version: 0.5+version: 0.5.0.1 synopsis: A simple library to call Alloy given a specification description: Please see the README on GitHub at <https://github.com/marcellussiegburg/call-alloy#readme> category: Language@@ -21,6 +21,9 @@ README.md LICENSE ChangeLog.md+ test/unit/readmeExampleInstance.hs+ test/unit/readmeExampleResult.hs+ test/unit/readmeExampleSpecification.als data-files: alloy/RunAlloy.class alloy/SATSolver.class
+ test/unit/readmeExampleInstance.hs view
@@ -0,0 +1,137 @@+fromList [+ ( Signature {scope = Nothing, sigName = "$withFlow_x"},+ Entry {+ annotation = Just Skolem,+ relation = fromList [+ ( "",+ Single (fromList [+ Object {objSig = "Node", identifier = 1}+ ]))+ ]+ }),+ ( Signature {scope = Nothing, sigName = "$withFlow_y"},+ Entry {+ annotation = Just Skolem,+ relation = fromList [+ ( "",+ Single (fromList [+ Object {objSig = "Node", identifier = 0}+ ]))+ ]+ }),+ ( Signature {scope = Nothing, sigName = "Int"},+ Entry {+ annotation = Nothing,+ relation = fromList [+ ( "",+ Single (fromList [+ NumberObject {number = -4},+ NumberObject {number = -3},+ NumberObject {number = -2},+ NumberObject {number = -1},+ NumberObject {number = 0},+ NumberObject {number = 1},+ NumberObject {number = 2},+ NumberObject {number = 3}+ ]))+ ]+ }),+ ( Signature {scope = Nothing, sigName = "String"},+ Entry {+ annotation = Nothing,+ relation = fromList [("", EmptyRelation)]+ }),+ ( Signature {scope = Nothing, sigName = "end"},+ Entry {+ annotation = Nothing,+ relation = fromList [+ ( "",+ Id (NumberObject {number = 0}))+ ]+ }),+ ( Signature {scope = Nothing, sigName = "integers"},+ Entry {+ annotation = Nothing,+ relation = fromList [+ ( "",+ Single (fromList [+ NumberObject {number = -4},+ NumberObject {number = -3},+ NumberObject {number = -2},+ NumberObject {number = -1},+ NumberObject {number = 0},+ NumberObject {number = 1},+ NumberObject {number = 2},+ NumberObject {number = 3}+ ]))+ ]+ }),+ ( Signature {scope = Nothing, sigName = "loop"},+ Entry {+ annotation = Nothing,+ relation = fromList [+ ( "",+ Id (NumberObject {number = 0}))+ ]+ }),+ ( Signature {scope = Nothing, sigName = "none"},+ Entry {+ annotation = Nothing,+ relation = fromList [("", EmptyRelation)]+ }),+ ( Signature {scope = Nothing, sigName = "univ"},+ Entry {+ annotation = Nothing,+ relation = fromList [+ ( "",+ Single (fromList [+ Object {objSig = "Node", identifier = 0},+ Object {objSig = "Node", identifier = 1},+ NumberObject {number = -4},+ NumberObject {number = -3},+ NumberObject {number = -2},+ NumberObject {number = -1},+ NumberObject {number = 0},+ NumberObject {number = 1},+ NumberObject {number = 2},+ NumberObject {number = 3}+ ]))+ ]+ }),+ ( Signature {scope = Just "seq", sigName = "Int"},+ Entry {+ annotation = Nothing,+ relation = fromList [+ ( "",+ Single (fromList [+ NumberObject {number = 0},+ NumberObject {number = 1},+ NumberObject {number = 2}+ ]))+ ]+ }),+ ( Signature {scope = Just "this", sigName = "Node"},+ Entry {+ annotation = Nothing,+ relation = fromList [+ ( "",+ Single (fromList [+ Object {objSig = "Node", identifier = 0},+ Object {objSig = "Node", identifier = 1}+ ])),+ ( "flow",+ Triple (fromList [+ ( Object {objSig = "Node", identifier = 1},+ Object {objSig = "Node", identifier = 0},+ NumberObject {number = 3})+ ])),+ ( "stored",+ Double (fromList [+ ( Object {objSig = "Node", identifier = 0},+ NumberObject {number = 0}),+ ( Object {objSig = "Node", identifier = 1},+ NumberObject {number = 1})+ ]))+ ]+ })+ ]
+ test/unit/readmeExampleResult.hs view
@@ -0,0 +1,7 @@+(+ fromList [Node 0,Node 1],+ fromList [(Node 0,0),(Node 1,1)],+ fromList [(Node 1,Node 0,3)],+ fromList [Node 1],+ fromList [Node 0]+ )
+ test/unit/readmeExampleSpecification.als view
@@ -0,0 +1,20 @@+abstract sig Node {+ flow : Node -> lone Int,+ stored : one Int+} {+ stored >= 0+ all n : Node | some flow[n] implies flow[n] >= 0+ no flow[this]+}++fun currentFlow(x, y : one Node) : Int {+ let s = x.stored, f = x.flow[y] | s < f implies s else f+}++pred withFlow[x, y : one Node] {+ currentFlow[x, y] > 0+}++pred show {}++run withFlow for 3 Int, 2 Node