Skip to content

Commit b89316f

Browse files
LunrtickLunrtick
committed
Add Haskell, update plot
1 parent 4e0debd commit b89316f

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

67 files changed

+7357
-3
lines changed

‎haskell/.gitignore

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
dist
2+
cabal-dev
3+
*.o
4+
*.hi
5+
*.chi
6+
*.chs.h
7+
*.dyn_o
8+
*.dyn_hi
9+
.virtualenv
10+
.hpc
11+
.hsenv
12+
*.prof
13+
*.aux
14+
*.hp
15+
.stack-work/
16+
*.csv
17+
*.tix
18+
stack.yaml.lock
19+
cudd-3.0.0

‎haskell/.gitlab-ci.yml

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
image: m4lvin/smcdel-ci:16.1
2+
3+
build:
4+
script:
5+
- stack --no-terminal test --coverage
6+
- stack --no-terminal bench --no-run-benchmarks

‎haskell/.travis.yml

+39
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
# Use new container infrastructure to enable caching
2+
sudo: false
3+
4+
# Do not choose a language; we provide our own build tools.
5+
language: generic
6+
7+
# Caching so the next build will be fast too.
8+
cache:
9+
directories:
10+
- $HOME/.stack
11+
12+
# Ensure necessary system libraries are present
13+
addons:
14+
apt:
15+
packages:
16+
- libgmp-dev
17+
- graphviz
18+
- poppler-utils
19+
- dot2tex
20+
- texlive-latex-base
21+
- preview-latex-style
22+
- texlive-pstricks
23+
24+
before_install:
25+
# Download and unpack the stack executable
26+
- mkdir -p ~/.local/bin
27+
- export PATH=$HOME/.local/bin:$PATH
28+
- travis_retry curl -L https://get.haskellstack.org/stable/linux-x86_64.tar.gz | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
29+
- stack --version
30+
31+
install:
32+
# Build dependencies
33+
- stack --no-terminal --install-ghc test --only-dependencies
34+
35+
script:
36+
# Build the package, its tests, and its docs and run the tests
37+
- stack --no-terminal test --coverage
38+
# check that benchmarks can be compile, but don't run them
39+
- stack --no-terminal bench --no-run-benchmarks

‎haskell/CHANGELOG.md

+62
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
# SMCDEL Changelog
2+
3+
## upcoming
4+
5+
New:
6+
7+
- "TRUE?" command in Web and CI interface
8+
9+
Changed:
10+
11+
- use HasCacBDD-0.1.0.3
12+
- update ace.js and MathJax
13+
14+
15+
## v1.1.0 (2019-12-09)
16+
17+
New:
18+
19+
- minimization under bisimulation
20+
- dynamic operators in formulas via `Data.Dynamic`
21+
- multipointed models, action models, structures and events
22+
- added Cheryl's Birthday and Cheryl's Age examples
23+
- experimental functions for epistemic planning (with small examples)
24+
- more instances for QuickCheck, more tests
25+
- add S5 to K conversion in `SMCDEL.Translations.Convert`
26+
- improvements to the web interface
27+
28+
Changed:
29+
30+
- polymorphic `update` replaces `productUpdate`, `transform`, `pubAnnounce` etc.
31+
- factual change by default: merge `Symbolic.S5.Change` into `Symbolic.S5` etc.
32+
- remove changeprops in (Kn)Trf to avoid redundancy with changelaw
33+
- move BDD related functions to HasCacBDD (`substit`, `substitSimul`)
34+
- avoid `Data.Map` in S5 modules, no longer depend on `lens`
35+
- replace `.cabal` file with a `package.yml` for `hpack`
36+
37+
38+
## v1.0.0 (2018-02-26)
39+
40+
New:
41+
42+
- action models and transformers with factual change
43+
- NonS5 modules, now called K, are no longer experimental
44+
- separate types State and World
45+
- automated testing and benchmarks
46+
- lots of bugfixes
47+
48+
Removed:
49+
50+
- removed support for robbed, NooBDD and Z3
51+
- old Example files
52+
53+
54+
## v0.2 (2015-11-17)
55+
56+
First release with a standalone-executable.
57+
58+
59+
## v0.1 (2015-09-21)
60+
61+
The first public version of SMCDEL. Note that this version does not contain a
62+
stand-alone executable. It can only be used as a Haskell library.

‎haskell/Dockerfile

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
FROM haskell:8.10
2+
WORKDIR /app
3+
COPY package.yaml stack.yaml stack.yaml.lock smcdel.cabal /app/
4+
RUN stack build --dependencies-only
5+
COPY src/ /app/src/
6+
COPY exec/ /app/exec/
7+
COPY static/ /app/static/
8+
COPY bench/ /app/bench/
9+
COPY Examples/ /app/Examples/
10+
RUN stack build --local-bin-path /app/bin/ --copy-bins
11+
COPY hyperfine /usr/bin/hyperfine
12+
ENV MIN_CHILDREN=3
13+
ENV MAX_CHILDREN=13
14+
ENV RESULTS_FILENAME="mc-haskell"
15+
ENV SYMBOLIC_OR_EXPLICIT="explicit"
16+
ENTRYPOINT hyperfine --warmup 1 -m 2 -M 50 --export-json /var/results/$RESULTS_FILENAME.json --parameter-scan num_children $MIN_CHILDREN $MAX_CHILDREN "./bin/smcdel-explicit-muddy $SYMBOLIC_OR_EXPLICIT {num_children}"

‎haskell/Examples/CherylsBirthday.smcdel.txt

+66
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
-- Cheryls Birthday in SMCDEL
2+
3+
VARS 5,6,7,8, -- month
4+
14,15,16,17,18,19 -- day of the month
5+
6+
LAW AND (
7+
-- birthday is one of these ten possibilities:
8+
OR ( (15 & 5), (16 & 5) , (19 & 5)
9+
, (17 & 6), (18 & 6)
10+
, (14 & 7), (16 & 7)
11+
, (14 & 8), (15 & 8), (17 & 8)
12+
),
13+
-- month must be unique:
14+
AND ( ~(5 & 6), ~(5 & 7), ~(5 & 8)
15+
, ~(6 & 7), ~(6 & 8)
16+
, ~(7 & 8)
17+
),
18+
-- days must be unique:
19+
AND ( ~(14 & 15), ~(14 & 16), ~(14 & 17), ~(14 & 18), ~(14 & 19)
20+
, ~(15 & 16), ~(15 & 17), ~(15 & 18), ~(15 & 19)
21+
, ~(16 & 17), ~(16 & 18), ~(16 & 19)
22+
, ~(17 & 18), ~(17 & 19)
23+
, ~(18 & 19)
24+
)
25+
)
26+
27+
OBS albert: 5,6,7,8 -- knows month
28+
bernard: 14,15,16,17,18,19 -- knows day
29+
30+
-- list all states
31+
WHERE?
32+
Top
33+
34+
-- the dialogue
35+
WHERE?
36+
-- Albert: I don't know when Cheryl's birthday is, ...
37+
< ! ~ OR ( albert knows that (15 & 5), albert knows that (16 & 5)
38+
, albert knows that (19 & 5), albert knows that (17 & 6)
39+
, albert knows that (18 & 6), albert knows that (14 & 7)
40+
, albert knows that (16 & 7), albert knows that (14 & 8)
41+
, albert knows that (15 & 8), albert knows that (17 & 8)
42+
) >
43+
-- ... but I know that Bernard doesn't know too.
44+
< ! ( albert knows that (
45+
~( OR ( bernard knows that (15 & 5), bernard knows that (16 & 5)
46+
, bernard knows that (19 & 5), bernard knows that (17 & 6)
47+
, bernard knows that (18 & 6), bernard knows that (14 & 7)
48+
, bernard knows that (16 & 7), bernard knows that (14 & 8)
49+
, bernard knows that (15 & 8), bernard knows that (17 & 8)
50+
) ) ) ) >
51+
-- Bernard: First I did not know when Cheryl's birthday is, but now I know.
52+
< ! OR ( bernard knows that (15 & 5), bernard knows that (16 & 5)
53+
, bernard knows that (19 & 5), bernard knows that (17 & 6)
54+
, bernard knows that (18 & 6), bernard knows that (14 & 7)
55+
, bernard knows that (16 & 7), bernard knows that (14 & 8)
56+
, bernard knows that (15 & 8), bernard knows that (17 & 8)
57+
) >
58+
-- Albert: Then I also know when Cheryl's birthday is.
59+
< ! OR ( albert knows that (15 & 5), albert knows that (16 & 5)
60+
, albert knows that (19 & 5), albert knows that (17 & 6)
61+
, albert knows that (18 & 6), albert knows that (14 & 7)
62+
, albert knows that (16 & 7), albert knows that (14 & 8)
63+
, albert knows that (15 & 8), albert knows that (17 & 8)
64+
) >
65+
-- (show all states where these announcements can be made in this order)
66+
Top

‎haskell/Examples/DiningCryptographers.smcdel.txt

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
-- Three Dining Cryptographers in SMCDEL
2+
3+
VARS 0, -- the NSA paid
4+
1,2,3, -- cryptographer i paid
5+
4,5,6 -- shared bits/coins
6+
7+
-- exactly one cryptographer or the NSA paid
8+
LAW AND ( OR (0,1,2,3), ~(0&1), ~(0&2), ~(0&3), ~(1&2), ~(1&3), ~(2&3) )
9+
10+
OBS alice: 1, 4,5
11+
bob : 2, 4, 6
12+
carol: 3, 5,6
13+
14+
VALID? (alice,bob,carol) comknow that (OR (0,1,2,3))
15+
16+
VALID? alice knows whether 1
17+
18+
VALID?
19+
[?! XOR (1, 4, 5)] -- After everyone announces the
20+
[?! XOR (2, 4, 6)] -- XOR of whether they paid and
21+
[?! XOR (3, 5, 6)] -- the coins they see ...
22+
AND (
23+
-- if the NSA paid this is common knowledge:
24+
0 -> (alice,bob,carol) comknow that 0,
25+
-- if one of the agents paid, the others don't know that:
26+
1 -> AND (~ bob knows that 1, ~ carol knows that 1),
27+
2 -> AND (~ alice knows that 2, ~ carol knows that 2),
28+
3 -> AND (~ alice knows that 3, ~ bob knows that 3)
29+
)

‎haskell/Examples/DrinkingLogicians.smcdel.txt

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
-- Three Drinking Logicians, see http://spikedmath.com/445.html
2+
3+
VARS 1,2,3
4+
5+
LAW Top
6+
7+
OBS a: 1
8+
b: 2
9+
c: 3
10+
11+
TRUE?
12+
{}
13+
a knows that ~(1 & 2 & 3)
14+
15+
VALID?
16+
[ ! ~ a knows whether (1 & 2 & 3) ]
17+
(a,b,c) comknow that 1
18+
19+
VALID?
20+
[ ! ~ a knows whether (1 & 2 & 3) ]
21+
[ ! ~ b knows whether (1 & 2 & 3) ]
22+
c knows whether (1 & 2 & 3)
23+
24+
VALID?
25+
( < ! ~ a knows whether (1 & 2 & 3) >
26+
< ! ~ b knows whether (1 & 2 & 3) >
27+
< ! c knows that (1 & 2 & 3) > Top )
28+
iff
29+
(1 & 2 & 3)

‎haskell/Examples/MuddyChildren.smcdel.txt

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
-- Three Muddy Children in SMCDEL
2+
3+
VARS 1,2,3
4+
5+
LAW Top
6+
7+
OBS alice: 2,3
8+
bob: 1, 3
9+
carol: 1,2
10+
11+
TRUE?
12+
{1,2,3}
13+
alice knows that (2 & 3) & ~ alice knows whether 1
14+
15+
VALID?
16+
( ~ (alice knows whether 1)
17+
& ~ (bob knows whether 2)
18+
& ~ (carol knows whether 3) )
19+
20+
WHERE?
21+
< ! (1|2|3) >
22+
( (alice knows whether 1)
23+
| (bob knows whether 2)
24+
| (carol knows whether 3) )
25+
26+
VALID?
27+
[ ! (1|2|3) ]
28+
[ ! ( (~ (alice knows whether 1))
29+
& (~ (bob knows whether 2))
30+
& (~ (carol knows whether 3)) ) ]
31+
[ ! ( (~ (alice knows whether 1))
32+
& (~ (bob knows whether 2))
33+
& (~ (carol knows whether 3)) ) ]
34+
(1 & 2 & 3)

0 commit comments

Comments
 (0)