Skip to content
This repository was archived by the owner on Jul 2, 2020. It is now read-only.

Commit dd6fadb

Browse files
praalhanspraalhans
committed
Initial commit
0 parents  commit dd6fadb

File tree

134 files changed

+15353
-0
lines changed

Some content is hidden

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

134 files changed

+15353
-0
lines changed

‎AUTHORS

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
List of authors (see also git history):
2+
3+
Hans-Dieter Hiep <hdh@cwi.nl>
4+
Centrum Wiskunde & Informatica
5+
6+
Wesley Shann
7+
Vrije Universiteit, Amsterdam
8+

‎DaVizFrege/.classpath

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<classpath>
3+
<classpathentry kind="src" path="src"/>
4+
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER">
5+
<attributes>
6+
<attribute name="module" value="true"/>
7+
</attributes>
8+
</classpathentry>
9+
<classpathentry kind="lib" path="/Users/wesleygenizshann/.p2/pool/plugins/frege.ide_3.25.42/lib/fregec.jar"/>
10+
<classpathentry kind="output" path="bin"/>
11+
</classpath>

‎DaVizFrege/.gitignore

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
# Compiled class file
2+
*.class
3+
4+
# Log file
5+
*.log
6+
7+
# BlueJ files
8+
*.ctxt
9+
10+
# Mobile Tools for Java (J2ME)
11+
.mtj.tmp/
12+
13+
# Package Files #
14+
*.jar
15+
*.war
16+
*.nar
17+
*.ear
18+
*.zip
19+
*.tar.gz
20+
*.rar
21+
22+
# virtual machine crash logs, see http://www.java.com/en/download/help/error_hotspot.xml
23+
hs_err_pid*
24+
25+
#
26+
.settings/
27+
bin/

‎DaVizFrege/.project

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<projectDescription>
3+
<name>DaVizFrege</name>
4+
<comment></comment>
5+
<projects>
6+
</projects>
7+
<buildSpec>
8+
<buildCommand>
9+
<name>org.eclipse.jdt.core.javabuilder</name>
10+
<arguments>
11+
</arguments>
12+
</buildCommand>
13+
<buildCommand>
14+
<name>frege.ide.frege.builder</name>
15+
<arguments>
16+
</arguments>
17+
</buildCommand>
18+
</buildSpec>
19+
<natures>
20+
<nature>org.eclipse.jdt.core.javanature</nature>
21+
<nature>frege.ide.frege.nature</nature>
22+
</natures>
23+
</projectDescription>

‎DaVizFrege/README.md

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
DaViz - Distributed Algorithms Visualization
2+
============================================
3+
4+
This is the Haskell implementation.
5+
6+
For the Java implementation, see the other project files.
7+
8+
The Frege port is a mirror of the main sources, made to compile with
9+
the Frege implementation of Haskell running on the JVM. The project
10+
is an Eclipse project. A recent version of Java is required (Java 8 or
11+
higher), and the following plug-in is used:
12+
13+
Frege Development Version 3.24.93
14+
15+
This can be obtained from: https://github.com/Frege/eclipse-plugin
16+
17+
The project can be imported in the Eclipse workspace by File > Import
18+
select General > Existing Project... and select the
19+
/java/ folder. The "DaVizFrege" project is for the Frege port
20+
and "DaViz" for Swing sources. Both should be imported. If Eclipse is
21+
installed with EGit, and the selected sources are under source control,
22+
you may also commit changes from Eclipse.
23+
24+
Due to the nature of the Frege plug-in, it may be necessary to delete
25+
a faulty reference to the Frege library, that points to a Windows path
26+
on the author's computer: context menu of DaVizFrege, select
27+
Properties and choose Java Build Path and the tab Libraries. Remove the
28+
offending fregec.jar reference. Afterwards, select the
29+
"Enable Frege Builder" action in the context menu of the project.
30+
31+
This should also be done for the "DaViz" project, if necessary, to
32+
enable running Frege compiled sources. However, only adding a Frege
33+
run-time library to that project is also sufficient, but left
34+
unexplored at the time of writing.

‎DaVizFrege/src/com/aexiz/daviz/sim/Awerbuch.fr

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
module com.aexiz.daviz.sim.Awerbuch where
2+
3+
import com.aexiz.daviz.sim.Set
4+
import com.aexiz.daviz.sim.Process
5+
6+
data RRRUII = ReceivedUnseen Channel
7+
| ReceivedSeen Channel
8+
| Replied Channel
9+
| Undefined
10+
| InitiatorUnseen
11+
| InitiatorSeen
12+
derive Eq RRRUII
13+
14+
-- Process state and message state spaces
15+
data PS = PS { hasToken :: Bool
16+
, state :: RRRUII
17+
, inform :: Set Channel
18+
, acked :: Set Channel
19+
, intended :: Maybe Channel
20+
, forward :: Set Channel
21+
, info :: Set Channel
22+
, last :: Maybe Channel
23+
, toAck :: Maybe Channel }
24+
data MS = Token | Inf | Ack
25+
type RS = Bool -- decide or terminate
26+
27+
-- State transition function
28+
trans :: PS -> ProcessResult RS PS MS
29+
-- Step 1.
30+
trans (PS True p ip ir (Just tf) n w Nothing Nothing) | sizeS ip > 0 =
31+
PSend s' (ch, Inf) where
32+
s' = PS True p (removeS ip ch) (addS ir ch) (Just tf) n w Nothing Nothing
33+
ch = nextS ip
34+
-- Step 2.
35+
trans (PS True p ip ir (Just tf) n w Nothing Nothing) | sizeS ip == 0 && sizeS ir == 0 && sizeS w == 0 =
36+
PSend s' (tf, Token) where
37+
s' = PS False p emptyS emptyS Nothing n w Nothing Nothing
38+
-- Step 3.
39+
trans (PS True p ip ir (Just tf) n w Nothing Nothing) | sizeS ip == 0 =
40+
PReceive f where
41+
f (rch, Ack) = let ch = reverseC rch in PS True p ip (removeS ir ch) (Just tf) n w Nothing Nothing
42+
f (_,_) = error "Unexpected message type (3)"
43+
-- Step 4.
44+
trans (PS True (ReceivedUnseen pa) ip ir Nothing n w Nothing Nothing) | sizeS ip == 0 && sizeS ir == 0 && sizeS n > 0 =
45+
PInternal [(PS True (ReceivedSeen pa) w' emptyS (Just ch) n' emptyS Nothing Nothing)] where
46+
ch = nextS n
47+
n' = removeS n ch
48+
w' = removeS w ch
49+
trans (PS True InitiatorUnseen ip ir Nothing n w Nothing Nothing) | sizeS ip == 0 && sizeS ir == 0 && sizeS n > 0 =
50+
PInternal [(PS True InitiatorSeen w' emptyS (Just ch) n' emptyS Nothing Nothing)] where
51+
ch = nextS n
52+
n' = removeS n ch
53+
w' = removeS w ch
54+
trans (PS True p ip ir Nothing n w Nothing Nothing) | sizeS ip == 0 && sizeS ir == 0 && sizeS n > 0 && sizeS w == 0 =
55+
PSend s' (ch, Token) where
56+
s' = PS False p emptyS emptyS Nothing n' w Nothing Nothing
57+
ch = nextS n
58+
n' = removeS n ch
59+
-- Step 5.
60+
trans (PS True (ReceivedUnseen pa) ip ir Nothing n w (Just ch) Nothing) | sizeS ip == 0 && sizeS ir == 0 =
61+
PInternal [(PS True (ReceivedSeen pa) w' emptyS (Just ch) n' emptyS Nothing Nothing)] where
62+
n' = removeS n ch
63+
w' = removeS w ch
64+
trans (PS True InitiatorUnseen ip ir Nothing n w (Just ch) Nothing) | sizeS ip == 0 && sizeS ir == 0 =
65+
PInternal [(PS True InitiatorSeen w' emptyS (Just ch) n' emptyS Nothing Nothing)] where
66+
n' = removeS n ch
67+
w' = removeS w ch
68+
trans (PS True p ip ir Nothing n w (Just ch) Nothing) | sizeS ip == 0 && sizeS ir == 0 && sizeS w == 0 =
69+
PSend s' (ch, Token) where
70+
s' = PS False p emptyS emptyS Nothing n' w Nothing Nothing
71+
n' = removeS n ch
72+
-- Step 6.
73+
trans (PS True (ReceivedUnseen pa) ip ir Nothing n w Nothing Nothing) | sizeS ip == 0 && sizeS ir == 0 && sizeS n == 0 =
74+
PInternal [(PS True (Replied pa) w emptyS (Just pa) emptyS emptyS Nothing Nothing)]
75+
trans (PS True (ReceivedSeen pa) ip ir Nothing n w Nothing Nothing) | sizeS ip == 0 && sizeS ir == 0 && sizeS n == 0 && sizeS w == 0 =
76+
PSend s' (pa, Token) where
77+
s' = (PS False (Replied pa) emptyS emptyS Nothing emptyS emptyS Nothing Nothing)
78+
-- Step 7.
79+
trans (PS True InitiatorSeen ip ir Nothing n w Nothing Nothing) | sizeS ip == 0 && sizeS ir == 0 && sizeS n == 0 && sizeS w == 0 =
80+
PResult True
81+
-- Step 8.
82+
trans (PS False (Replied _) ip ir Nothing n w Nothing Nothing) | sizeS ip == 0 && sizeS ir == 0 && sizeS n == 0 && sizeS w == 0 =
83+
PResult False
84+
trans (PS False Undefined ip ir Nothing n w Nothing Nothing) | sizeS ip == 0 && sizeS ir == 0 && sizeS n == 0 && sizeS w == 0 =
85+
PResult False
86+
-- Step 9 & 10.
87+
trans (PS False p ip ir Nothing n w m Nothing) | sizeS ip == 0 && sizeS ir == 0 =
88+
PReceive f where
89+
-- Step 9.
90+
f (rch, Token) | p == Undefined = let ch = reverseC rch in
91+
PS True (ReceivedUnseen ch) emptyS emptyS Nothing (removeS n ch) (removeS w ch) Nothing Nothing
92+
f (rch, Token) | otherwise = let ch = reverseC rch in case member ch n of
93+
True -> PS True p emptyS emptyS Nothing n w (Just ch) Nothing
94+
False -> PS True p emptyS emptyS Nothing n w Nothing Nothing
95+
-- Step 10.
96+
f (rch, Inf) = let ch = reverseC rch in PS False p emptyS emptyS Nothing (removeS n ch) w m (Just ch)
97+
-- Partial
98+
f (_,_) = error "Unexpected message type (9,10)"
99+
trans (PS False p ip ir Nothing n w m (Just ch)) | sizeS ip == 0 && sizeS ir == 0 =
100+
PSend s' (ch, Ack) where
101+
s' = (PS False p ip ir Nothing n w m Nothing)
102+
-- Partial
103+
trans _ = error "Underspecified"
104+
105+
procDesc :: Process -> ProcessDescription KnownNetwork RS PS MS
106+
procDesc i = PD init trans where
107+
init (n, p) | p == i = PS True InitiatorUnseen emptyS emptyS Nothing (outChannels n p) (outChannels n p) Nothing Nothing
108+
| otherwise = PS False Undefined emptyS emptyS Nothing (outChannels n p) (outChannels n p) Nothing Nothing
109+

‎DaVizFrege/src/com/aexiz/daviz/sim/Cidon.fr

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
module com.aexiz.daviz.sim.Cidon where
2+
3+
import com.aexiz.daviz.sim.Set
4+
import com.aexiz.daviz.sim.Process
5+
6+
data RRUI = Received Channel
7+
| Replied Channel
8+
| Undefined
9+
| Initiator
10+
derive Eq RRUI
11+
12+
-- Process state and message state spaces
13+
data PS = PS { hasToken :: Bool
14+
, state :: RRUI
15+
, intention :: Maybe Channel
16+
, forward :: Set Channel
17+
, info :: Set Channel }
18+
data MS = Token | Inf
19+
type RS = Bool
20+
21+
22+
-- State transition function
23+
trans :: PS -> ProcessResult RS PS MS
24+
-- Step 1.
25+
trans (PS True (Received pa) Nothing p i) | (sizeS p) > 0 =
26+
PInternal [s'] where
27+
x = nextS p
28+
s' = (PS True (Received pa) (Just x) (removeS p x) (removeS i x))
29+
trans (PS True Initiator Nothing p i) | (sizeS p) > 0 =
30+
PInternal [s'] where
31+
x = nextS p
32+
s' = (PS True Initiator (Just x) (removeS p x) (removeS i x))
33+
-- Step 2.
34+
trans (PS True (Received ch) (Just x) p i) | (sizeS i) > 0 =
35+
PSend s' (im, Inf) where
36+
im = nextS i
37+
s' = (PS True (Received ch) (Just x) p (removeS i im))
38+
trans (PS True Initiator (Just x) p i) | (sizeS i) > 0 =
39+
PSend s' (im, Inf) where
40+
im = nextS i
41+
s' = (PS True Initiator (Just x) p (removeS i im))
42+
-- Step 3.
43+
trans (PS True (Received ch) (Just x) p i) | (sizeS i) == 0 =
44+
PSend s' (x, Token) where
45+
s' = (PS False (Received ch) (Just x) p emptyS)
46+
trans (PS True Initiator (Just x) p i) | (sizeS i) == 0 =
47+
PSend s' (x, Token) where
48+
s' = (PS False Initiator (Just x) p emptyS)
49+
-- Step 4a. (see notes)
50+
trans (PS True (Received ch) Nothing p i) | (sizeS p) == 0 && (sizeS i) > 0 =
51+
PSend s' (im, Inf) where
52+
im = nextS i
53+
s' = (PS True (Received ch) Nothing emptyS (removeS i im))
54+
-- Step 4.
55+
trans (PS True (Received ch) Nothing p i) | (sizeS p) == 0 && (sizeS i) == 0 =
56+
PSend s' (ch, Token) where
57+
s' = (PS False (Replied ch) Nothing emptyS emptyS)
58+
-- Step 5.
59+
trans (PS True Initiator Nothing p i) | (sizeS p) == 0 && (sizeS i) == 0 =
60+
PResult True
61+
-- Step 6.
62+
trans (PS False (Replied ch) Nothing p i) | (sizeS p) == 0 && (sizeS i) == 0 =
63+
PResult False
64+
-- Step 7.
65+
trans (PS False Undefined Nothing p i) =
66+
PReceive f where
67+
f (rch, Token) = let ch = reverseC rch in (PS True (Received ch) Nothing (removeS p ch) (removeS i ch))
68+
f (rch, Inf) = (PS False Undefined Nothing (removeS p (reverseC rch)) i)
69+
-- Step 8 & 9.
70+
trans (PS False (Received pa) (Just x) p i) =
71+
PReceive f where
72+
f (rch, _) | (reverseC rch) == x = (PS True (Received pa) Nothing p i)
73+
| otherwise = (PS False (Received pa) (Just x) (removeS p (reverseC rch)) i)
74+
trans (PS False Initiator (Just x) p i) =
75+
PReceive f where
76+
f (rch, _) | (reverseC rch) == x = (PS True Initiator Nothing p i)
77+
| otherwise = (PS False Initiator (Just x) (removeS p (reverseC rch)) i)
78+
-- Step 10 & 11.
79+
trans (PS False (Received pa) Nothing p i) =
80+
PReceive f where
81+
f (rch, Token) = (PS True (Received pa) Nothing p i)
82+
f (rch, Inf) = (PS False (Received pa) Nothing (removeS p (reverseC rch)) i)
83+
trans (PS False Initiator Nothing p i) =
84+
PReceive f where
85+
f (rch, Token) = (PS True Initiator Nothing p i)
86+
f (rch, Inf) = (PS False Initiator Nothing (removeS p (reverseC rch)) i)
87+
-- Partial
88+
trans _ = error "Underspecified"
89+
90+
procDesc :: Process -> ProcessDescription KnownNetwork RS PS MS
91+
procDesc i = PD init trans where
92+
init (n, p) | p == i = PS True Initiator Nothing (outChannels n p) (outChannels n p)
93+
| otherwise = PS False Undefined Nothing (outChannels n p) (outChannels n p)
94+

‎DaVizFrege/src/com/aexiz/daviz/sim/DFS.fr

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
module com.aexiz.daviz.sim.DFS where
2+
3+
import com.aexiz.daviz.sim.Set
4+
import com.aexiz.daviz.sim.Process
5+
6+
data RRUI = Received Channel
7+
| Replied Channel
8+
| Undefined
9+
| Initiator
10+
derive Eq RRUI
11+
12+
-- Process state and message state spaces
13+
type PS = (Bool, RRUI, Set Channel, Maybe Channel)
14+
type MS = () -- token
15+
type RS = Bool -- decide or terminate
16+
17+
-- State transition function
18+
trans :: PS -> ProcessResult RS PS MS
19+
-- procDesc (token, parent, neighbors left, incoming channel)
20+
-- Step 1.
21+
trans (True, p, n, Nothing) | sizeS n > 0 = PSend s' (ch, tok) where
22+
s' = (False, p, n', Nothing)
23+
n' = removeS n ch
24+
ch = nextS n
25+
tok = ()
26+
-- Step 2.
27+
trans (True, p, n, Just ch) = PSend s' (ch, tok) where
28+
s' = (False, p, n', Nothing)
29+
n' = removeS n ch
30+
tok = ()
31+
-- Step 3.
32+
trans (True, Received ch, n, Nothing) | sizeS n == 0 = PSend s' (ch, tok) where
33+
s' = (False, Replied ch, n, Nothing)
34+
tok = ()
35+
-- Step 4.
36+
trans (True, Initiator, n, Nothing) | sizeS n == 0 = PResult True
37+
-- Step 5.
38+
trans (False, Replied _, n, Nothing) | sizeS n == 0 = PResult False
39+
trans (False, Undefined, n, Nothing) | sizeS n == 0 = PResult False
40+
-- Step 6.
41+
trans (False, Undefined, n, m) = PReceive f where
42+
f (rch, tok) = let ch = reverseC rch in (True, Received ch, removeS n ch, Nothing)
43+
trans (False, p, n, m) = PReceive f where
44+
f (rch, tok) = let ch = reverseC rch in case member ch n of
45+
True -> (True, p, removeS n ch, Just ch)
46+
False -> (True, p, n, Nothing)
47+
-- Partial
48+
trans _ = error "Underspecified"
49+
50+
procDesc :: Process -> ProcessDescription KnownNetwork RS PS MS
51+
procDesc i = PD init trans where
52+
init (n, p) | p == i = (True, Initiator, outChannels n p, Nothing)
53+
| otherwise = (False, Undefined, outChannels n p, Nothing)
54+

0 commit comments

Comments
 (0)