Skip to content

Commit

Permalink
feat: compute EBEs (#4)
Browse files Browse the repository at this point in the history
  • Loading branch information
fahchen authored Aug 2, 2024
1 parent 7c14c76 commit 078d283
Show file tree
Hide file tree
Showing 26 changed files with 2,095 additions and 69 deletions.
2 changes: 1 addition & 1 deletion .credo.exs
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ exclude_test_files = {:files, %{excluded: ["test/", "apps/*/test/"]}}
#
## Readability Checks
#
{Credo.Check.Readability.AliasOrder, []},
{Credo.Check.Readability.AliasOrder, [sort_method: :ascii]},
{Credo.Check.Readability.FunctionNames, []},
{Credo.Check.Readability.LargeNumbers, []},
{Credo.Check.Readability.MaxLineLength, [priority: :low, max_length: 120]},
Expand Down
2 changes: 1 addition & 1 deletion .formatter.exs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
locals_without_parens = [colset: 1, var: 1, val: 1]
locals_without_parens = [colset: 1, var: 1, val: 1, return: 1]

[
inputs: ["{mix,.formatter}.exs", "{config,lib,test}/**/*.{ex,exs}"],
Expand Down
2 changes: 1 addition & 1 deletion lib/coloured_flow/definition/action.ex
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ defmodule ColouredFlow.Definition.Action do

field :inputs, [Variable.name()],
doc: """
The available variables includes the variables in the in-going places,
The available variables includes the variables in the in-coming places,
and the constants. The variables in the out-going isn't available.
"""

Expand Down
17 changes: 12 additions & 5 deletions lib/coloured_flow/definition/arc.ex
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ defmodule ColouredFlow.Definition.Arc do
use TypedStructor

alias ColouredFlow.Definition.Expression
alias ColouredFlow.Definition.Place
alias ColouredFlow.Definition.Transition

@type name() :: binary()

Expand All @@ -23,17 +25,22 @@ defmodule ColouredFlow.Definition.Arc do
- `:p_to_t`: from a place to a transition
"""

field :transition, Transition.name()
field :place, Place.name()

field :expression, Expression.t(),
doc: """
The expression that is used to evaluate the arc.
When a transition is fired, the tokens in the in-going places are matched
with the in-going arcs will be consumed, and the tokens in the out-going places
When a transition is fired, the tokens in the in-coming places are matched
with the in-coming arcs will be consumed, and the tokens in the out-going places
are updated with the out-going arcs.
Note that the in-going arcs can't refer to an unbound variable,
howerver, the out-going arcs can refer to an unbound variable that has to be
updated by the action of the transition.
Note that incoming arcs cannot refer to an unbound variable,
but they can refer to variables bound by other incoming arcs
(see <https://cpntools.org/2018/01/09/resource-allocation-example/>).
However, outgoing arcs are allowed to refer to an unbound variable
that will be updated during the transition action.
"""
end
end
4 changes: 2 additions & 2 deletions lib/coloured_flow/definition/colour_set/descr.ex
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ defmodule ColouredFlow.Definition.ColourSet.Descr do

# map
defp valid?({:map, types}) when is_map(types) and map_size(types) >= 1 do
Enum.all?(types, fn {_, type} -> valid?(type) end)
Enum.all?(types, fn {key, type} when is_atom(key) -> valid?(type) end)
end

# enum
Expand All @@ -42,7 +42,7 @@ defmodule ColouredFlow.Definition.ColourSet.Descr do

# union
defp valid?({:union, types}) when is_map(types) and map_size(types) >= 2 do
Enum.all?(types, fn {_, type} -> valid?(type) end)
Enum.all?(types, fn {tag, type} when is_atom(tag) -> valid?(type) end)
end

# list
Expand Down
2 changes: 1 addition & 1 deletion lib/coloured_flow/definition/coloured_petri_net.ex
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ defmodule ColouredFlow.Definition.ColouredPetriNet do

typed_structor enforce: true do
# data types
field :colour_sets, [ColourSet.t()], default: []
field :colour_sets, [ColourSet.t()]

# net
field :places, [Place.t()]
Expand Down
76 changes: 75 additions & 1 deletion lib/coloured_flow/definition/expression.ex
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,85 @@ defmodule ColouredFlow.Definition.Expression do
An expression is a quoted Elixir expression that can be evaluated
"""

alias ColouredFlow.Definition.ColourSet
alias ColouredFlow.Definition.Variable

use TypedStructor

@type returning() :: {
non_neg_integer() | {:cpn_returning_variable, Variable.name()},
{:cpn_returning_variable, Variable.name()} | ColourSet.value()
}

typed_structor enforce: true do
plugin TypedStructor.Plugins.DocFields

field :expr, Macro.t(), doc: "a quoted expression"
field :expr, Macro.t(),
default: nil,
doc: "a quoted expression, `nil` is a valid expression that does nothing."

field :vars, [Variable.name()],
default: [],
doc: """
a list of variables that are used in the expression,
when the expression is evaluated, the variables will
be bound to the values that are passed in.
"""

field :returnings,
list(returning()),
default: [],
doc: """
The result that are returned by the arc, is form of a multi-set of tokens.
- `[{1, {:cpn_returning_variable, :x}}]`: return 1 token of colour `:x`
- `[{2, {:cpn_returning_variable, :x}}, {3, {:cpn_returning_variable, :y}}]`: return 2 tokens of colour `:x` or 3 tokens of colour `:y`
- `[{:x, {:cpn_returning_variable, :y}}]`: return `x` tokens of colour `:y`
- `[{0, {:cpn_returning_variable, :x}}]`: return 0 tokens (empty tokens) of colour `:x`
"""
end

@spec build(binary() | nil) ::
{:ok, t()}
| {:error, ColouredFlow.Expression.compile_error()}
def build(expr) when is_nil(expr) when expr === "", do: {:ok, %__MODULE__{}}

def build(expr) when is_binary(expr) do
with(
{:ok, quoted, vars, returnings} <- ColouredFlow.Expression.compile(expr, __ENV__),
{:ok, returnings} <- check_returning_vars(vars, returnings)
) do
{:ok, %__MODULE__{expr: quoted, vars: Map.keys(vars), returnings: returnings}}
end
end

defp check_returning_vars(vars, returnings) do
returning_vars = Enum.flat_map(returnings, &ColouredFlow.Expression.Returning.get_var_names/1)
returning_vars = Map.new(returning_vars)
vars = Enum.map(vars, &elem(&1, 0))
diff = Map.drop(returning_vars, vars)

case Map.to_list(diff) do
[] ->
{:ok, Enum.map(returnings, &ColouredFlow.Expression.Returning.prune_meta/1)}

[{name, meta} | _rest] ->
{
:error,
{
meta,
"missing returning variable in vars: #{inspect(name)}",
""
}
}
end
end

@spec build!(binary() | nil) :: t()
def build!(expr) do
case build(expr) do
{:ok, expr} -> expr
{:error, reason} -> raise reason
end
end
end
2 changes: 1 addition & 1 deletion lib/coloured_flow/definition/transition.ex
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
defmodule ColouredFlow.Definition.Transition do
@moduledoc """
Transition t is enabled at a binding if there are tokens
matching the values of the in-going arc inscriptions and
matching the values of the in-coming arc inscriptions and
the guard of t evaluates to true.
"""

Expand Down
80 changes: 80 additions & 0 deletions lib/coloured_flow/enabled_binding_elements/binding.ex
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
defmodule ColouredFlow.EnabledBindingElements.Binding do
@moduledoc """
The utility functions for bindings.
"""

alias ColouredFlow.Definition.ColourSet
alias ColouredFlow.Definition.Variable

@typep binding() :: [{Variable.name(), ColourSet.value()}]

@doc """
Get the conflicts between two bindings.
## Examples
iex> get_conflicts([{:x, 1}, {:y, 2}], [{:x, 1}, {:y, 3}])
[{:y, {2, 3}}]
iex> get_conflicts([x: 0, y: 3], [y: 2])
[y: {3, 2}]
iex> get_conflicts([y: 2], [x: 0, y: 3])
[y: {2, 3}]
iex> get_conflicts([], [{:x, 1}, {:y, 2}])
[]
iex> get_conflicts([{:x, 1}, {:y, 2}], [{:z, 3}])
[]
"""
@spec get_conflicts(binding1 :: binding(), binding2 :: binding()) ::
[{Variable.name(), {ColourSet.value(), ColourSet.value()}}]
def get_conflicts(binding1, []) when is_list(binding1), do: []
def get_conflicts([], binding2) when is_list(binding2), do: []

def get_conflicts(binding1, binding2) when is_list(binding1) and is_list(binding2) do
binding1 = Map.new(binding1)
binding2 = Map.new(binding2)

conflicts =
Map.intersect(binding1, binding2, fn _k, v1, v2 ->
{v1, v2}
end)

Enum.filter(conflicts, fn {_key, {v1, v2}} -> v1 != v2 end)
end

@doc """
Compute combinations of bindings that do not conflict.
## Examples
iex> combine([[[x: 1, y: 2], [x: 1, y: 3]], [[x: 1], [x: 3]]])
[[y: 2, x: 1], [y: 3, x: 1]]
iex> combine([[[x: 1, y: 2], [x: 1, y: 3]], [[x: 1], [x: 3]], [[z: 1], [z: 2]]])
[[y: 3, x: 1, z: 2], [y: 3, x: 1, z: 1], [y: 2, x: 1, z: 2], [y: 2, x: 1, z: 1]]
iex> combine([[[x: 1, y: 2], [x: 1, y: 3]], [[x: 1], [x: 3]], [[y: 3]]])
[[x: 1, y: 3]]
iex> combine([[[x: 1, y: 2]], [[x: 1, y: 3]]])
[]
iex> combine([[[x: 1, y: 2]]])
[[x: 1, y: 2]]
"""
@spec combine(bindings_list :: [[binding()]]) :: [binding()]
def combine(bindings_list) do
Enum.reduce(bindings_list, [[]], fn bindings, prevs ->
for prev <- prevs, binding <- bindings, reduce: [] do
acc ->
case get_conflicts(prev, binding) do
[] -> [Keyword.merge(prev, binding) | acc]
_other -> acc
end
end
end)
end
end
Loading

0 comments on commit 078d283

Please sign in to comment.