Skip to content

Commit

Permalink
Allow field conditions without then clause
Browse files Browse the repository at this point in the history
Ref. #95
  • Loading branch information
treiher committed Oct 14, 2020
1 parent 8468de5 commit ad5c1a7
Show file tree
Hide file tree
Showing 6 changed files with 92 additions and 7 deletions.
3 changes: 2 additions & 1 deletion doc/Language-Reference.md
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,7 @@ A message type is a collection components. Additional then clauses allow to defi
*message_definition* ::= __message__ [ *null_component* ] *component* { *component* } __end message__ | __null message__

*component* ::= *component_name* __:__ *component_type*
[__if__ *condition*]
{ *then_clause* } __;__

*null_component* ::= __null__
Expand All @@ -108,7 +109,7 @@ A message type is a collection components. Additional then clauses allow to defi

#### Static Semantics

A message type specifies the message format of a protocol. Each component corresponds to one field in a message. A then clause of a component allows to define which field follows. If no then clause is given, it is assumed that always the next component of the message follows. If no further component follows, it is assumed that the message ends with this field. The end of a message can also be denoted explicitly by adding a then clause to __null__. Optionally a then clause can contain a condition under which the corresponding field follows and aspects which allow to define the length of the next field and the location of its first bit. The condition can refer to previous fields (including the component containing the then clause). If required, a null component can be used to specify the length of the first field in the message. An empty message can be represented by a null message.
A message type specifies the message format of a protocol. Each component corresponds to one field in a message. A then clause of a component allows to define which field follows. If no then clause is given, it is assumed that always the next component of the message follows. If no further component follows, it is assumed that the message ends with this field. The end of a message can also be denoted explicitly by adding a then clause to __null__. Optionally a then clause can contain a condition under which the corresponding field follows and aspects which allow to define the length of the next field and the location of its first bit. The condition can refer to previous fields (including the component containing the then clause). A condition can also be added to a component. A component condition is equivalent to adding a condition to all incoming then clauses. If a component condition as well as a condition at an incoming then clause exists, both conditions are combined by a logical conjunction. If required, a null component can be used to specify the length of the first field in the message. An empty message can be represented by a null message.

#### Example

Expand Down
4 changes: 2 additions & 2 deletions rflx/model/message.py
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
from abc import abstractmethod
from collections import defaultdict
from copy import copy
from dataclasses import dataclass
from dataclasses import dataclass, field as dataclass_field
from typing import Any, Dict, List, Mapping, Optional, Sequence, Set, Tuple

import rflx.typing_ as rty
Expand Down Expand Up @@ -52,7 +52,7 @@ class Link(Base):
condition: expr.Expr = expr.TRUE
length: expr.Expr = expr.UNDEFINED
first: expr.Expr = expr.UNDEFINED
location: Optional[Location] = None
location: Optional[Location] = dataclass_field(default=None, repr=False)

def __str__(self) -> str:
condition = indent_next(
Expand Down
7 changes: 6 additions & 1 deletion rflx/specification/ast.py
Original file line number Diff line number Diff line change
Expand Up @@ -41,11 +41,16 @@ def __eq__(self, other: object) -> bool:

class Component(SyntaxTree):
def __init__(
self, name: StrID = None, type_name: StrID = None, thens: List[Then] = None
self,
name: StrID = None,
type_name: StrID = None,
thens: List[Then] = None,
condition: Expr = TRUE,
) -> None:
self.name = ID(name) if name else None
self.type_name = ID(type_name) if type_name else None
self.thens = thens or []
self.condition = condition


@dataclass
Expand Down
3 changes: 2 additions & 1 deletion rflx/specification/grammar.py
Original file line number Diff line number Diff line change
Expand Up @@ -442,11 +442,12 @@ def message_type_definition() -> Token:
- unqualified_identifier()
+ Literal(":")
- qualified_identifier()
- Optional(if_condition(restricted=True), TRUE)
- then_list
- semicolon()
)
component_item.setParseAction(
lambda t: Component(t[0], t[2], t[3]) if len(t) >= 4 else Component(t[0], t[2])
lambda t: Component(t[0], t[2], t[4], t[3]) if len(t) >= 5 else Component(t[0], t[2])
)
component_item.setName("Component")
null_component_item = Keyword("null") - then - semicolon()
Expand Down
15 changes: 13 additions & 2 deletions rflx/specification/parser.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@

from pyparsing import ParseException, ParseFatalException

import rflx.expression as expr
from rflx.error import (
RecordFluxError,
Severity,
Expand All @@ -14,7 +15,6 @@
pop_source,
push_source,
)
from rflx.expression import UNDEFINED
from rflx.identifier import ID
from rflx.model import (
BUILTIN_TYPES,
Expand Down Expand Up @@ -267,6 +267,8 @@ def create_message(
skip_verification: bool,
cache: Cache,
) -> Message:
# pylint: disable=too-many-locals

components = list(message.components)

if components and components[0].name:
Expand Down Expand Up @@ -296,7 +298,7 @@ def create_message(
then.first.location,
)
for then in component.thens
if then.first != UNDEFINED
if then.first != expr.UNDEFINED
]
)

Expand All @@ -307,6 +309,15 @@ def create_message(
target_node = Field(name) if name else FINAL
structure.append(Link(source_node, target_node))

if component.condition != expr.TRUE:
for l in structure:
if l.target.identifier == component.name:
l.condition = (
expr.And(component.condition, l.condition, location=l.condition.location)
if l.condition != expr.TRUE
else component.condition
)

for then in component.thens:
target_node = Field(then.name) if then.name else FINAL
if then.name and target_node not in field_types.keys():
Expand Down
67 changes: 67 additions & 0 deletions tests/unit/specification/parser_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,13 @@
from rflx import expression as expr, model
from rflx.error import Location, RecordFluxError, Severity, Subsystem, fail
from rflx.identifier import ID
from rflx.model import FINAL, INITIAL, Field, Link, Message, ModularInteger
from rflx.specification import ast, cache, parser
from tests.const import EX_SPEC_DIR, SPEC_DIR
from tests.data import models

T = ModularInteger("Test::T", expr.Number(256))


def assert_specifications_files(
filenames: Sequence[str], specifications: Mapping[str, ast.Specification]
Expand Down Expand Up @@ -1120,3 +1123,67 @@ def test_create_model_checksum() -> None:
)
],
}


@pytest.mark.parametrize(
"spec",
[
"""
type M is
message
A : T
then B
if A < 100;
B : T
if A > 10;
end message;
""",
"""
type M is
message
A : T;
B : T
if A > 10 and A < 100;
end message;
""",
"""
type M is
message
A : T
then B
if A > 10 and A < 100;
B : T;
end message;
""",
],
)
def test_message_field_condition(spec: str) -> None:
assert_messages_string(
f"""
package Test is
type T is mod 256;
{spec}
end Test;
""",
[
Message(
"Test::M",
[
Link(INITIAL, Field("A")),
Link(
Field("A"),
Field("B"),
condition=expr.And(
expr.Greater(expr.Variable("A"), expr.Number(10)),
expr.Less(expr.Variable("A"), expr.Number(100)),
),
),
Link(Field("B"), FINAL),
],
{Field("A"): T, Field("B"): T},
),
],
)

0 comments on commit ad5c1a7

Please sign in to comment.