Skip to content

Commit

Permalink
Add CARDINALITY connective to MEF and PDAG
Browse files Browse the repository at this point in the history
Issue #234
  • Loading branch information
rakhimov committed Jan 28, 2018
1 parent 8d4f3ec commit 21f82d2
Show file tree
Hide file tree
Showing 13 changed files with 332 additions and 22 deletions.
75 changes: 66 additions & 9 deletions src/event.cc
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@

#include "event.h"

#include <limits>

#include <boost/range/algorithm.hpp>

#include "error.h"
Expand Down Expand Up @@ -92,16 +94,12 @@ void Formula::ArgSet::Remove(ArgEvent event) {
}

Formula::Formula(Connective connective, ArgSet args,
std::optional<int> min_number)
std::optional<int> min_number, std::optional<int> max_number)
: connective_(connective),
min_number_(min_number ? min_number.value() : 0),
min_number_(min_number.value_or(0)),
max_number_(max_number.value_or(0)),
args_(std::move(args)) {
if (min_number && connective_ != kAtleast) {
SCRAM_THROW(LogicError(
"The min number can only be defined for 'atleast' connective. "
"The connective of this formula is '" +
std::string(kConnectiveToString[connective_]) + "'."));
}
ValidateMinMaxNumber(min_number, max_number);

switch (connective_) {
case kAnd:
Expand Down Expand Up @@ -142,18 +140,45 @@ Formula::Formula(Connective connective, ArgSet args,
"than its min number " +
std::to_string(min_number_) + "."));
}
break;
case kCardinality:
if (!min_number || !max_number)
SCRAM_THROW(ValidityError(
"'cardinality' connective requires min and max number for args."));

if (min_number_ > max_number_)
SCRAM_THROW(ValidityError("\"cardinality\" connective min number (" +
std::to_string(min_number_) +
") cannot be greater than max number (" +
std::to_string(max_number_) + ")."));
if (args_.empty())
SCRAM_THROW(ValidityError(
"\"cardinality\" connective requires one or more arguments."));

if (args_.size() < max_number_)
SCRAM_THROW(
ValidityError("\"cardinality\" connective max number (" +
std::to_string(max_number_) +
") cannot be greater than the number of arguments (" +
std::to_string(args_.size()) + ")"));
}

for (const Arg& arg : args_.data())
ValidateNesting(arg);
}

std::optional<int> Formula::min_number() const {
if (connective_ == kAtleast)
if (connective_ == kAtleast || connective_ == kCardinality)
return min_number_;
return {};
}

std::optional<int> Formula::max_number() const {
if (connective_ == kCardinality)
return max_number_;
return {};
}

void Formula::Swap(ArgEvent current, ArgEvent other) {
auto it = boost::find_if(args_.data(), [&current](const Arg& arg) {
return arg.event == current;
Expand All @@ -177,6 +202,38 @@ void Formula::Swap(ArgEvent current, ArgEvent other) {
it->event.swap(other);
}

void Formula::ValidateMinMaxNumber(std::optional<int> min_number,
std::optional<int> max_number) {
assert(!min_number ||
std::numeric_limits<decltype(min_number_)>::max() >= *min_number);
assert(!max_number ||
std::numeric_limits<decltype(max_number_)>::max() >= *max_number);

if (min_number) {
if (*min_number < 0)
SCRAM_THROW(LogicError("The min number cannot be negative."));

if (connective_ != kAtleast && connective_ != kCardinality) {
SCRAM_THROW(LogicError(
"The min number can only be defined for 'atleast' "
"or 'cardinality' connective. The connective of this formula is '" +
std::string(kConnectiveToString[connective_]) + "'."));
}
}

if (max_number) {
if (*max_number < 0)
SCRAM_THROW(LogicError("The max number cannot be negative."));

if (connective_ != kCardinality) {
SCRAM_THROW(LogicError(
"The max number can only be defined for 'cardinality' connective. "
"The connective of this formula is '" +
std::string(kConnectiveToString[connective_]) + "'."));
}
}
}

void Formula::ValidateNesting(const Arg& arg) {
if (arg.complement) {
if (connective_ == kNull || connective_ == kNot)
Expand Down
36 changes: 28 additions & 8 deletions src/event.h
Original file line number Diff line number Diff line change
Expand Up @@ -215,17 +215,18 @@ enum Connective : std::uint8_t {

// Rarely used connectives specific to the MEF.
kIff, ///< Equality with two inputs only.
kImply ///< Implication with two inputs only.
kImply, ///< Implication with two inputs only.
kCardinality ///< General quantifier of events.
};

/// The number of connectives in the enum.
const int kNumConnectives = 10;
const int kNumConnectives = 11;

/// String representations of the connectives.
/// The ordering is the same as the Connective enum.
const char* const kConnectiveToString[] = {"and", "or", "atleast", "xor",
"not", "nand", "nor", "null",
"iff", "imply"};
const char* const kConnectiveToString[] = {"and", "or", "atleast", "xor",
"not", "nand", "nor", "null",
"iff", "imply", "cardinality"};

/// Boolean formula with connectives and arguments.
/// Formulas are not expected to be shared.
Expand Down Expand Up @@ -288,18 +289,24 @@ class Formula {
/// @returns The number of arguments in the set.
std::size_t size() const { return args_.size(); }

/// @return true if the set is empty.
bool empty() const { return args_.empty(); }

private:
std::vector<Arg> args_; ///< The underlying data container.
};

/// @param[in] connective The logical connective for this Boolean formula.
/// @param[in] args The arguments of the formula.
/// @param[in] min_number The min number relevant to the connective.
/// @param[in] max_number The max number relevant to the connective.
///
/// @throws ValidityError Invalid arguments or setup for the connective.
/// @throws LogicError Invalid nesting of complement or constant args.
/// @throws LogicError Negative values for min or max number.
Formula(Connective connective, ArgSet args,
std::optional<int> min_number = {});
std::optional<int> min_number = {},
std::optional<int> max_number = {});

/// Copy semantics only.
/// @{
Expand All @@ -310,9 +317,12 @@ class Formula {
/// @returns The connective of this formula.
Connective connective() const { return connective_; }

/// @returns The min number for "atleast" connective.
/// @returns The min number for "atleast"/"cardinality" connective.
std::optional<int> min_number() const;

/// @returns The max number of "cardinality" connective.
std::optional<int> max_number() const;

/// @returns The arguments of this formula.
const std::vector<Arg>& args() const { return args_.data(); }

Expand All @@ -331,6 +341,15 @@ class Formula {
void Swap(ArgEvent current, ArgEvent other);

private:
/// Validates the min and max numbers relevant to the connective.
///
/// @param[in] min_number The number to be used for connective min number.
/// @param[in] max_number The number to be used for connective max number.
///
/// @throws LogicError The min or max number is invalid or not applicable.
void ValidateMinMaxNumber(std::optional<int> min_number,
std::optional<int> max_number);

/// Checks if the formula argument results in invalid nesting.
///
/// @param[in] arg The argument in the formula.
Expand All @@ -339,7 +358,8 @@ class Formula {
void ValidateNesting(const Arg& arg);

Connective connective_; ///< Logical connective.
int min_number_; ///< Min number for "atleast" connective.
std::uint16_t min_number_; ///< Min number for "atleast"/"cardinality".
std::uint16_t max_number_; ///< Max number for "cardinality".
ArgSet args_; ///< All events.
};

Expand Down
3 changes: 2 additions & 1 deletion src/event_tree_analysis.cc
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,8 @@ Clone(const mef::Formula& formula,
arg_set.Add(std::visit(cloner, arg.event), arg.complement);

return std::make_unique<mef::Formula>(
formula.connective(), std::move(arg_set), formula.min_number());
formula.connective(), std::move(arg_set), formula.min_number(),
formula.max_number());
}

} // namespace
Expand Down
3 changes: 2 additions & 1 deletion src/initializer.cc
Original file line number Diff line number Diff line change
Expand Up @@ -805,7 +805,8 @@ FormulaPtr Initializer::GetFormula(const xml::Element& formula_node,

try {
return std::make_unique<Formula>(formula_type, std::move(arg_set),
formula_node.attribute<int>("min"));
formula_node.attribute<int>("min"),
formula_node.attribute<int>("max"));
} catch (ValidityError& err) {
err << boost::errinfo_at_line(formula_node.line());
throw;
Expand Down
30 changes: 30 additions & 0 deletions src/pdag.cc
Original file line number Diff line number Diff line change
Expand Up @@ -663,6 +663,36 @@ GatePtr Pdag::ConstructComplexGate(const mef::Formula& formula, bool ccf,
formula.args().back().complement, ccf, nodes);
return parent;
}
case mef::kCardinality: {
assert(formula.args().size() >= *formula.max_number());
assert(*formula.min_number() <= *formula.max_number());
normal_ = false;
auto parent = std::make_shared<Gate>(kAnd, this);
auto first_arg = std::make_shared<Gate>(kAtleast, this);
first_arg->min_number(*formula.min_number());
for (const mef::Formula::Arg& arg : formula.args()) {
AddArg(first_arg, arg.event, arg.complement, ccf, nodes);
}
auto second_arg = first_arg->Clone();
second_arg->NegateArgs();
second_arg->min_number(formula.args().size() - *formula.max_number());

auto well_form = [](Gate* atleast) {
if (atleast->min_number() == 0) {
atleast->MakeConstant(true);
} else if (atleast->min_number() == 1) {
atleast->type(kOr);
} else if (atleast->min_number() == atleast->args().size()) {
atleast->type(kAnd);
}
};
well_form(first_arg.get());
well_form(second_arg.get());

parent->AddArg(first_arg);
parent->AddArg(second_arg);
return parent;
}
default:
assert(false && "Unexpected connective for complex gates.");
}
Expand Down
26 changes: 25 additions & 1 deletion tests/bench_core_tests.cc
Original file line number Diff line number Diff line change
Expand Up @@ -393,12 +393,36 @@ TEST_P(RiskAnalysisTest, ImplyABC) {
EXPECT_EQ(3, products().size());
EXPECT_EQ(pi, products());
} else {
std::set<std::set<std::string>> mcs = {{"A"}, {"B"}, {"C"}};
EXPECT_EQ(1, products().size());
CHECK(products().begin()->empty());
}
}

// Benchmark Tests for cardinality #(1, 2, [A, B, C]) fault tree.
TEST_P(RiskAnalysisTest, CardinalityABC) {
std::string tree_input = "tests/input/core/cardinality.xml";
settings.probability_analysis(true);
ASSERT_NO_THROW(ProcessInputFiles({tree_input}));
ASSERT_NO_THROW(analysis->Analyze());
if (settings.approximation() == Approximation::kRareEvent) {
EXPECT_DOUBLE_EQ(0.6, p_total());
} else {
EXPECT_DOUBLE_EQ(0.49, p_total());
}

if (settings.prime_implicants()) {
std::set<std::set<std::string>> pi = {{"B", "not A"}, {"C", "not B"},
{"A", "not C"}, {"C", "not A"},
{"A", "not B"}, {"B", "not C"}};
EXPECT_EQ(6, products().size());
EXPECT_EQ(pi, products());
} else {
std::set<std::set<std::string>> mcs = {{"A"}, {"B"}, {"C"}};
EXPECT_EQ(3, products().size());
EXPECT_EQ(mcs, products());
}
}

// Checks for top gate of NOT with a single basic event child.
TEST_P(RiskAnalysisTest, NotA) {
std::string tree_input = "tests/input/core/not_a.xml";
Expand Down
34 changes: 32 additions & 2 deletions tests/event_tests.cc
Original file line number Diff line number Diff line change
Expand Up @@ -64,17 +64,19 @@ TEST_CASE("BasicEventTest.Validate", "[mef::event]") {
CHECK_THROWS_AS(event.Validate(), ValidityError);
}

TEST_CASE("FormulaTest.MinNumber", "[mef::event]") {
TEST_CASE("FormulaTest.MinMaxNumber", "[mef::event]") {
BasicEvent first_child("first");
BasicEvent second_child("second");

SECTION("Invalid connective") {
Formula::ArgSet arg_set = {&first_child, &second_child};
CHECK_THROWS_AS(Formula(kAnd, arg_set, 2), LogicError);
CHECK_THROWS_AS(Formula(kAnd, arg_set, 2, 3), LogicError);

Formula top(kAnd, arg_set);
CHECK(top.connective() == kAnd);
CHECK(top.min_number() == std::nullopt);
CHECK(top.max_number() == std::nullopt);
}

SECTION("Atleast") {
Expand All @@ -85,13 +87,41 @@ TEST_CASE("FormulaTest.MinNumber", "[mef::event]") {
CHECK(top.min_number() == 2);
// No min number.
CHECK_THROWS_AS(Formula(kAtleast, arg_set), ValidityError);
// Redundant max number.
CHECK_THROWS_AS(Formula(kAtleast, arg_set, 2, 3), LogicError);
CHECK_THROWS_AS(Formula(kAtleast, arg_set, {}, 3), LogicError);
// Illegal min number.
CHECK_THROWS_AS(Formula(kAtleast, arg_set, -2), ValidityError);
CHECK_THROWS_AS(Formula(kAtleast, arg_set, -2), LogicError);
CHECK_THROWS_AS(Formula(kAtleast, arg_set, 1), ValidityError);
CHECK_THROWS_AS(Formula(kAtleast, arg_set, 0), ValidityError);
CHECK_THROWS_AS(Formula(kAtleast, arg_set, 3), ValidityError);
CHECK_THROWS_AS(Formula(kAtleast, arg_set, 4), ValidityError);
}

SECTION("Cardinality") {
BasicEvent third_child("third");
Formula::ArgSet arg_set = {&first_child, &second_child, &third_child};
Formula top(kCardinality, arg_set, 2, 3);
CHECK(top.connective() == kCardinality);
CHECK(top.min_number() == 2);
CHECK(top.max_number() == 3);

CHECK_THROWS_AS(Formula(kCardinality, arg_set), ValidityError);
CHECK_THROWS_AS(Formula(kCardinality, arg_set, 2), ValidityError);
CHECK_THROWS_AS(Formula(kCardinality, arg_set, {}, 2), ValidityError);
CHECK_THROWS_AS(Formula(kCardinality, arg_set, -2, 3), LogicError);
CHECK_THROWS_AS(Formula(kCardinality, arg_set, 2, -3), LogicError);
CHECK_THROWS_AS(Formula(kCardinality, arg_set, 2, 4), ValidityError);
CHECK_THROWS_AS(Formula(kCardinality, arg_set, 2, 1), ValidityError);

CHECK_NOTHROW(Formula(kCardinality, arg_set, 0, 0));
CHECK_NOTHROW(Formula(kCardinality, arg_set, 0, 2));
CHECK_NOTHROW(Formula(kCardinality, arg_set, 2, 2));

// Empty args.
CHECK_THROWS_AS(Formula(kCardinality, {}, 0, 0), ValidityError);
CHECK_THROWS_AS(Formula(kCardinality, {}, 0, 1), ValidityError);
}
}

TEST_CASE("FormulaTest.EventArguments", "[mef::event]") {
Expand Down
1 change: 1 addition & 0 deletions tests/initializer_tests.cc
Original file line number Diff line number Diff line change
Expand Up @@ -272,6 +272,7 @@ TEST_CASE("InitializerTest.IncorrectFtaInputs", "[mef::initializer]") {
"def_clash_basic_house.xml",
"def_clash_house_basic.xml",
"atleast_gate.xml",
"invalid_min_max_cardinality.xml",
"cyclic_tree.xml",
"cyclic_formula.xml",
"cyclic_parameter.xml",
Expand Down
21 changes: 21 additions & 0 deletions tests/input/core/cardinality.xml
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
<?xml version="1.0"?>
<opsa-mef>
<define-fault-tree name="Cardinality">
<define-gate name="TopEvent">
<cardinality min="1" max="2">
<event name="A" type="basic-event"/>
<event name="B" type="basic-event"/>
<event name="C" type="basic-event"/>
</cardinality>
</define-gate>
<define-basic-event name="A">
<float value="0.1"/>
</define-basic-event>
<define-basic-event name="B">
<float value="0.2"/>
</define-basic-event>
<define-basic-event name="C">
<float value="0.3"/>
</define-basic-event>
</define-fault-tree>
</opsa-mef>
Loading

0 comments on commit 21f82d2

Please sign in to comment.