diff --git a/wepl/acp.pl b/wepl/access-control-policy.pl similarity index 100% rename from wepl/acp.pl rename to wepl/access-control-policy.pl diff --git a/wepl/ackermann.pl b/wepl/ackerman.pl similarity index 100% rename from wepl/ackermann.pl rename to wepl/ackerman.pl diff --git a/wepl/age.pl b/wepl/age-checker.pl similarity index 100% rename from wepl/age.pl rename to wepl/age-checker.pl diff --git a/wepl/bmt.pl b/wepl/basic-monadic-benchmark.pl similarity index 100% rename from wepl/bmt.pl rename to wepl/basic-monadic-benchmark.pl diff --git a/wepl/dt.pl b/wepl/deep-taxonomy.pl similarity index 100% rename from wepl/dt.pl rename to wepl/deep-taxonomy.pl diff --git a/wepl/dining-philosophers.pl b/wepl/dining-philosophers.pl new file mode 100644 index 000000000..8e28d9bc8 --- /dev/null +++ b/wepl/dining-philosophers.pl @@ -0,0 +1,41 @@ +% Dining Philosophers +% See http://www.cs.utk.edu/~plank/plank/classes/cs560/560/notes/Dphil/lecture.html + +''('', '', ''). +''('', '', ''). +''('', '', ''). +''('', '', ''). +''('', '', ''). + +''(A) :- + ''(A, B, C), + mutex_lock(B), + mutex_lock(C). + +''(A) :- + ''(A, B, C), + mutex_unlock(C), + mutex_unlock(B). + +''(A, B, C) :- + sleep(B), + format('% ~w thinking for ~w seconds~n', [A, B]), + ''(A), + sleep(C), + format('% ~w eating for ~w seconds~n', [A, C]), + ''(A). + +''('', '') :+ + thread_create(''('', 0.1, 0.1), A, []), + thread_create(''('', 0.2, 0.2), B, []), + thread_create(''('', 0.15, 0.1), C, []), + thread_create(''('', 0.25, 0.2), D, []), + thread_create(''('', 0.25, 0.1), E, []), + thread_join(A, _), + thread_join(B, _), + thread_join(C, _), + thread_join(D, _), + thread_join(E, _). + +% query +true :+ ''('', ''). diff --git a/wepl/fft.pl b/wepl/fast-fourier-transform.pl similarity index 100% rename from wepl/fft.pl rename to wepl/fast-fourier-transform.pl diff --git a/wepl/fourcolor.pl b/wepl/four-color.pl similarity index 100% rename from wepl/fourcolor.pl rename to wepl/four-color.pl diff --git a/wepl/gcc.pl b/wepl/gray-code-counter.pl similarity index 100% rename from wepl/gcc.pl rename to wepl/gray-code-counter.pl diff --git a/wepl/lee.pl b/wepl/lee-routing.pl similarity index 100% rename from wepl/lee.pl rename to wepl/lee-routing.pl diff --git a/wepl/mi.pl b/wepl/meta-interpretation.pl similarity index 100% rename from wepl/mi.pl rename to wepl/meta-interpretation.pl diff --git a/wepl/output/acp.pl b/wepl/output/access-control-policy.pl similarity index 100% rename from wepl/output/acp.pl rename to wepl/output/access-control-policy.pl diff --git a/wepl/output/ackermann.pl b/wepl/output/ackerman.pl similarity index 100% rename from wepl/output/ackermann.pl rename to wepl/output/ackerman.pl diff --git a/wepl/output/age.pl b/wepl/output/age-checker.pl similarity index 100% rename from wepl/output/age.pl rename to wepl/output/age-checker.pl diff --git a/wepl/output/bmt.pl b/wepl/output/basic-monadic-benchmark.pl similarity index 100% rename from wepl/output/bmt.pl rename to wepl/output/basic-monadic-benchmark.pl diff --git a/wepl/output/dt.pl b/wepl/output/deep-taxonomy.pl similarity index 100% rename from wepl/output/dt.pl rename to wepl/output/deep-taxonomy.pl diff --git a/wepl/output/dining-philosophers.pl b/wepl/output/dining-philosophers.pl new file mode 100644 index 000000000..e6b3af886 --- /dev/null +++ b/wepl/output/dining-philosophers.pl @@ -0,0 +1,32 @@ +:- op(1200, xfx, :+). + +% thinking for 0.1 seconds +% thinking for 0.15 seconds +% thinking for 0.2 seconds +% eating for 0.1 seconds +% thinking for 0.25 seconds +% thinking for 0.25 seconds +% eating for 0.1 seconds +% eating for 0.2 seconds +% eating for 0.2 seconds +% eating for 0.1 seconds +% thinking for 0.1 seconds +% thinking for 0.15 seconds +% thinking for 0.2 seconds +% eating for 0.1 seconds +% thinking for 0.25 seconds +% eating for 0.1 seconds +% thinking for 0.25 seconds +% eating for 0.2 seconds +% eating for 0.2 seconds +% eating for 0.1 seconds +% answers + answer(''('', '')). + +% proof steps + step((''('', ''):+thread_create(''('', 0.1, 0.1), A, []), thread_create(''('', 0.2, 0.2), B, []), thread_create(''('', 0.15, 0.1), C, []), thread_create(''('', 0.25, 0.2), D, []), thread_create(''('', 0.25, 0.1), E, []), thread_join(A, _), thread_join(B, _), thread_join(C, _), thread_join(D, _), thread_join(E, _)), + (thread_create(''('', 0.1, 0.1), '$BLOB'("(3,0x564742e252c0)"), []), thread_create(''('', 0.2, 0.2), '$BLOB'("(4,0x564742e25310)"), []), thread_create(''('', 0.15, 0.1), '$BLOB'("(5,0x564742e25360)"), []), thread_create(''('', 0.25, 0.2), '$BLOB'("(6,0x564742e253b0)"), []), thread_create(''('', 0.25, 0.1), '$BLOB'("(7,0x564742e24d70)"), []), thread_join('$BLOB'("(3,0x564742e252c0)"), true), thread_join('$BLOB'("(4,0x564742e25310)"), true), thread_join('$BLOB'("(5,0x564742e25360)"), true), thread_join('$BLOB'("(6,0x564742e253b0)"), true), thread_join('$BLOB'("(7,0x564742e24d70)"), true)), + ''('', '')). + step((true:+''('', '')), + ''('', ''), + true). diff --git a/wepl/output/fft.pl b/wepl/output/fast-fourier-transform.pl similarity index 100% rename from wepl/output/fft.pl rename to wepl/output/fast-fourier-transform.pl diff --git a/wepl/output/fourcolor.pl b/wepl/output/four-color.pl similarity index 100% rename from wepl/output/fourcolor.pl rename to wepl/output/four-color.pl diff --git a/wepl/output/gcc.pl b/wepl/output/gray-code-counter.pl similarity index 100% rename from wepl/output/gcc.pl rename to wepl/output/gray-code-counter.pl diff --git a/wepl/output/lee.pl b/wepl/output/lee-routing.pl similarity index 100% rename from wepl/output/lee.pl rename to wepl/output/lee-routing.pl diff --git a/wepl/output/mi.pl b/wepl/output/meta-interpretation.pl similarity index 100% rename from wepl/output/mi.pl rename to wepl/output/meta-interpretation.pl diff --git a/wepl/output/sdcoding.pl b/wepl/output/superdense-coding.pl similarity index 100% rename from wepl/output/sdcoding.pl rename to wepl/output/superdense-coding.pl diff --git a/wepl/output/tak.pl b/wepl/output/takeuchi.pl similarity index 100% rename from wepl/output/tak.pl rename to wepl/output/takeuchi.pl diff --git a/wepl/sdcoding.pl b/wepl/superdense-coding.pl similarity index 100% rename from wepl/sdcoding.pl rename to wepl/superdense-coding.pl diff --git a/wepl/tak.pl b/wepl/takeuchi.pl similarity index 100% rename from wepl/tak.pl rename to wepl/takeuchi.pl