Skip to content

Commit

Permalink
synthesis: add greedy best first search (GBFS)
Browse files Browse the repository at this point in the history
topology: append vars
stage: move `plan_lts_state` back
action instantiations: add FetchPermutation()
action instantiations: remove `MarkUsed()`
  • Loading branch information
nightly committed Aug 6, 2023
1 parent 7924a61 commit 19cdb70
Show file tree
Hide file tree
Showing 39 changed files with 645 additions and 102 deletions.
2 changes: 2 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ This tool provides **controller synthesis**/orchestration of resource programs $

Logical action theories for resource programs are given by **situation calculus** basic action theories, $\mathcal{D_i}$. Situation calculus is a second-order logic with equality for reasoning about actions in AI with three disjoint sorts: *actions*, *objects*, and *situations*. **Preconditions** are specified for each action (and possibly for certain configurations of compound/concurrent actions), and **successor state axioms** encode causal laws of changes to fluents as a result of performing actions (dynamic predicates).

This tool implements three different possible search algorithms for controller synthesis, namely: **A* search**, **Greedy Best First Search** (GBFS), and **Simple Parallel A* (shared frontier)** (SPA*, experimental).

## Build instructions
### Requirements
- [CMake](https://cmake.org/) (>=3.26)
Expand Down
11 changes: 7 additions & 4 deletions app/scs.cpp
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
#include <iostream>

#include "programs/programs.h"
#include "Hinge/run.h"
#include "HingeQuick/run.h"
#include "Hinge/Full/run.h"
#include "Hinge/Quick/run.h"
#include "Hinge/Extended/run.h"
#include "scs/Common/timer.h"
#include "scs/Common/windows.h"

Expand All @@ -15,12 +16,14 @@ int main(int argc, const char* argv[]) {
scs::SetConsoleEncoding();
// LogModeTrace();

ExecutionType type = ExecutionType::AStar;
size_t example = 1;
ExecutionType type = ExecutionType::GBFS;
size_t example = 2;

if (example == 1) {
scs::examples::RunHingeQuick(type);
} else if (example == 2) {
scs::examples::RunHinge(type);
} else if (example == 3) {
scs::examples::RunHingeExtended(type);
}
}
3 changes: 2 additions & 1 deletion bench/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,8 @@ package_add_benchmark("BenchScCompoundAction" "SituationCalculus/compound_action
package_add_benchmark("BenchSynthHingeExpansion" "Synthesis/Hinge/expansion.cpp")
package_add_benchmark("BenchSynthHingeTopology" "Synthesis/Hinge/topology.cpp")

package_add_benchmark("BenchSynthHingeController" "Synthesis/Hinge/controller.cpp")
package_add_benchmark("BenchSynthHingeControllerQuick" "Synthesis/Hinge/controller_quick.cpp")
package_add_benchmark("BenchSynthHingeControllerFull" "Synthesis/Hinge/controller_full.cpp")
package_add_benchmark("BenchSynthHingeControllerExtended" "Synthesis/Hinge/controller_extended.cpp")


64 changes: 64 additions & 0 deletions bench/Synthesis/Hinge/controller_extended.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
#include <benchmark/benchmark.h>
#include "Hinge/hinge.h"
#include "Hinge/Extended/recipe.h"

using namespace scs;
using namespace scs::examples;

class HingeControllerExtended : public benchmark::Fixture {
protected:
std::unique_ptr<ITopology> topology;
std::vector<CharacteristicGraph> graphs;
scs::BasicActionTheory global;
CharacteristicGraph graph_recipe;
protected:
void SetUp(const ::benchmark::State& state) {

auto resource1 = HingeResource1();
graphs.emplace_back(resource1.program, ProgramType::Resource);

auto resource2 = HingeResource2();
graphs.emplace_back(resource2.program, ProgramType::Resource);

auto resource3 = HingeResource3();
graphs.emplace_back(resource3.program, ProgramType::Resource);

auto resource4 = HingeResource4();
graphs.emplace_back(resource4.program, ProgramType::Resource);

auto common = HingeCommon();
auto common_bat = HingeCommonBAT();
topology = std::make_unique<CompleteTopology>(&graphs, true);

CoopMatrix cm(10);
cm.Add(1, 2);
cm.Add(1, 3);
cm.Add(2, 3);
RoutesMatrix rm(10);
rm.Add(1, 2);

std::vector<scs::BasicActionTheory> bats{common_bat, resource1.bat, resource2.bat, resource3.bat, resource4.bat};
global = CombineBATs(bats, cm, rm);

auto recipe_prog = HingeExtendedRecipe();
graph_recipe = CharacteristicGraph(recipe_prog, ProgramType::Recipe);
}

void TearDown(const ::benchmark::State& state) {

}

};

BENCHMARK_DEFINE_F(HingeControllerExtended, AStar)(benchmark::State& state) {
Limits lim{ .global_transition_limit = 50, .global_cost_limit = 200,
.stage_transition_limit = 4, .stage_cost_limit = 50, .fairness_limit = 20 };
Best best(graphs, graph_recipe, global, *topology, lim);

for (auto _ : state) {
auto controller = best.Synthethise();
benchmark::DoNotOptimize(controller);
benchmark::ClobberMemory();
}
}
BENCHMARK_REGISTER_F(HingeControllerExtended, AStar)->Unit(benchmark::kMillisecond);
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
#include <benchmark/benchmark.h>
#include "Hinge/hinge.h"
#include "Hinge/recipe.h"
#include "Hinge/Full/recipe.h"

using namespace scs;
using namespace scs::examples;

class HingeController : public benchmark::Fixture {
class HingeControllerFull : public benchmark::Fixture {
protected:
std::unique_ptr<ITopology> topology;
std::vector<CharacteristicGraph> graphs;
Expand Down Expand Up @@ -50,7 +50,7 @@ class HingeController : public benchmark::Fixture {

};

BENCHMARK_DEFINE_F(HingeController, AStar)(benchmark::State& state) {
BENCHMARK_DEFINE_F(HingeControllerFull, AStar)(benchmark::State& state) {
Limits lim{ .global_transition_limit = 50, .global_cost_limit = 200,
.stage_transition_limit = 4, .stage_cost_limit = 50, .fairness_limit = 20 };
Best best(graphs, graph_recipe, global, *topology, lim);
Expand All @@ -61,4 +61,4 @@ BENCHMARK_DEFINE_F(HingeController, AStar)(benchmark::State& state) {
benchmark::ClobberMemory();
}
}
BENCHMARK_REGISTER_F(HingeController, AStar)->Unit(benchmark::kMillisecond);
BENCHMARK_REGISTER_F(HingeControllerFull, AStar)->Unit(benchmark::kMillisecond);
20 changes: 16 additions & 4 deletions bench/Synthesis/Hinge/controller_quick.cpp
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
#include <benchmark/benchmark.h>
#include "Hinge/hinge.h"
#include "Hinge/recipe.h"
#include "HingeQuick/recipe.h"
#include "Hinge/Quick/recipe.h"

using namespace scs;
using namespace scs::examples;
Expand Down Expand Up @@ -62,5 +61,18 @@ BENCHMARK_DEFINE_F(HingeControllerQuick, AStar)(benchmark::State& state) {
benchmark::ClobberMemory();
}
}
BENCHMARK_REGISTER_F(HingeControllerQuick, AStar)->Unit(benchmark::kMillisecond)->Iterations(10);
// 134 ms
BENCHMARK_REGISTER_F(HingeControllerQuick, AStar)->Unit(benchmark::kMillisecond)->Iterations(50);
// 6.25 ms

BENCHMARK_DEFINE_F(HingeControllerQuick, GBFS)(benchmark::State& state) {
Limits lim{ .global_transition_limit = 10, .global_cost_limit = 200,
.stage_transition_limit = 3, .stage_cost_limit = 50, .fairness_limit = 20 };
GBFS gbfs(graphs, graph_recipe, global, *topology, lim);

for (auto _ : state) {
auto controller = gbfs.Synthethise();
benchmark::DoNotOptimize(controller);
benchmark::ClobberMemory();
}
}
BENCHMARK_REGISTER_F(HingeControllerQuick, GBFS)->Unit(benchmark::kMillisecond)->Iterations(50);
46 changes: 46 additions & 0 deletions examples/Hinge/Extended/recipe.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
#pragma once

#include <iostream>
#include <format>

#include "scs/SituationCalculus/situation_calculus.h"
#include "scs/Common/strings.h"
#include "scs/FirstOrderLogic/fol.h"
#include "scs/ConGolog/Program/programs.h"
#include "scs/ConGolog/resource.h"

/*
#Program
Load(brass) || Load(tube);
Paint(brass, metallic blue) | Paint(brass, metallic red);
Clamp(brass) ||| RadialDrill(brass, 5);
ApplyAdhesive(tube, brass);
*/

namespace scs::examples {

inline std::shared_ptr<IProgram> HingeExtendedRecipe() {
scs::ActionProgram LoadBrass{scs::Action{"Load", {Object{"brass"}} }};
scs::ActionProgram LoadTube{scs::Action{"Load", {Object{"tube"}} }};

scs::ActionProgram PaintBlue{scs::Action{"Paint", { Object{"brass"}, Object{"metallic_red"} }}};
scs::ActionProgram PaintRed{scs::Action{"Paint", { Object{"brass"}, Object{"metallic_blue"} }}};

scs::ActionProgram Clamp{scs::Action{"Clamp", { Object{"brass"} }}};
scs::ActionProgram RadialDrill{scs::Action{"RadialDrill", { Object{"brass"}, Object{"5mm"}}}};

scs::ActionProgram ApplyAdhesive{scs::Action{"ApplyAdhesive", { Object{"tube"}, Object{"brass"} }}};

// ------ //

Interleaved interleaved(LoadBrass, LoadTube);
Branch nd1(PaintBlue, PaintRed);
Simultaneous sim1(Clamp, RadialDrill);

Sequence stage1(interleaved, nd1);
Sequence stage2(stage1, sim1);
Sequence stage3(stage2, ApplyAdhesive);

return std::make_shared<Sequence>(stage3);
}
}
112 changes: 112 additions & 0 deletions examples/Hinge/Extended/run.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,112 @@
#pragma once

#include "recipe.h"
#include "Hinge/resource_1.h"
#include "Hinge/resource_2.h"
#include "Hinge/resource_3.h"
#include "Hinge/resource_4.h"
#include "Hinge/common.h"

#include "scs/Common/timer.h"
#include "scs/ConGolog/CharacteristicGraph/characteristic_graph.h"
#include "scs/Synthesis/synthesis.h"
#include "scs/Common/windows.h"
#include "execution_type.h"

namespace scs::examples {

void RunHingeExtended(const ExecutionType& exec) {
std::string dir;
if (exec == ExecutionType::AStar) {
dir = "Hinge/Extended/AStar/";
} else if (exec == ExecutionType::GBFS) {
dir = "Hinge/Extended/GBFS/";
} else if (exec == ExecutionType::SPA) {
dir = "Hinge/Extended/SPA/";
}

// ------- Load BATs, Cg --------
std::vector<CharacteristicGraph> graphs;
auto common = HingeCommon();
auto common_bat = HingeCommonBAT();

auto resource1 = HingeResource1();
graphs.emplace_back(resource1.program, ProgramType::Resource);
ExportGraph(graphs.back(), dir + "Resource1");

auto resource2 = HingeResource2();
graphs.emplace_back(resource2.program, ProgramType::Resource);
ExportGraph(graphs.back(), dir + "Resource2");

auto resource3 = HingeResource3();
graphs.emplace_back(resource3.program, ProgramType::Resource);
ExportGraph(graphs.back(), dir + "Resource3");

auto resource4 = HingeResource4();
graphs.emplace_back(resource4.program, ProgramType::Resource);
ExportGraph(graphs.back(), dir + "Resource4");

auto recipe_prog = HingeExtendedRecipe();
CharacteristicGraph graph_recipe(recipe_prog, ProgramType::Recipe);
ExportGraph(graph_recipe, dir + "Recipe");

// ------------------------------

// ----- Coop & Routes -----
CoopMatrix cm(10);
cm.Add(1, 2);
cm.Add(1, 3);
cm.Add(2, 3);
RoutesMatrix rm(10);
rm.Add(1, 2);
rm.Add(2, 4);
rm.Add(1, 4);

// -------------------------

// ------ Global BAT -------
std::vector<scs::BasicActionTheory> bats{common_bat, resource1.bat, resource2.bat, resource3.bat, resource4.bat};
auto global = CombineBATs(bats, cm, rm);
// -------------------------

// std::cout << common.within_reach;
// std::cout << global.successors["part"].Form() << std::endl;
// std::cout << global.pre["In"].Form() << std::endl;

// std::cout << global;
// std::cout << global.Initial();
// std::cout << *graphs[3].lts.states().at(2).key_;
// -------------------------------

Limits lim { .global_transition_limit = 50, .global_cost_limit = 200,
.stage_transition_limit = 4, .stage_cost_limit = 50, .fairness_limit = 20};

Timer topology_timer("Topology time");
CompleteTopology topology(&graphs, false);
topology_timer.StopWithWrite();

if (1) {
if (exec == ExecutionType::AStar) {
Best best(graphs, graph_recipe, global, topology, lim);
auto controller = best.Synthethise();
ExportController(controller.value().plan, dir + "Controller");
} else if (exec == ExecutionType::GBFS) {
GBFS gbfs(graphs, graph_recipe, global, topology, lim);
auto controller = gbfs.Synthethise();
ExportController(controller.value().plan, dir + "Controller");
} else if (exec == ExecutionType::SPA) {
SPA spa(graphs, graph_recipe, global, topology, lim);
auto controller = spa.Synthethise();
ExportController(controller.value().plan, dir + "Controller");
}
}

ExportTopology(topology, dir + "Topology");
if (exec == ExecutionType::AStar) {
GenerateImagesFromDot("../../exports/Hinge/Extended/AStar/");
} else if (exec == ExecutionType::SPA) {
GenerateImagesFromDot("../../exports/Hinge/Extended/SPA/");
}

}
}
9 changes: 9 additions & 0 deletions examples/Hinge/Extended/run.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
#pragma once

#include "execution_type.h"

namespace scs::examples {

void RunHingeExtended(const ExecutionType& exec = ExecutionType::AStar);

}
File renamed without changes.
18 changes: 13 additions & 5 deletions examples/Hinge/run.cpp → examples/Hinge/Full/run.cpp
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
#pragma once

#include "recipe.h"
#include "resource_1.h"
#include "resource_2.h"
#include "resource_3.h"
#include "resource_4.h"
#include "common.h"
#include "Hinge/resource_1.h"
#include "Hinge/resource_2.h"
#include "Hinge/resource_3.h"
#include "Hinge/resource_4.h"
#include "Hinge/common.h"

#include "scs/Common/timer.h"
#include "scs/ConGolog/CharacteristicGraph/characteristic_graph.h"
Expand All @@ -19,6 +19,8 @@ namespace scs::examples {
std::string dir;
if (exec == ExecutionType::AStar) {
dir = "Hinge/Full/AStar/";
} else if (exec == ExecutionType::GBFS) {
dir = "Hinge/Full/GBFS/";
} else if (exec == ExecutionType::SPA) {
dir = "Hinge/Full/SPA/";
}
Expand Down Expand Up @@ -82,6 +84,10 @@ namespace scs::examples {
Best best(graphs, graph_recipe, global, topology, lim);
auto controller = best.Synthethise();
ExportController(controller.value().plan, dir + "Controller");
} else if (exec == ExecutionType::GBFS) {
GBFS gbfs(graphs, graph_recipe, global, topology, lim);
auto controller = gbfs.Synthethise();
ExportController(controller.value().plan, dir + "Controller");
} else if (exec == ExecutionType::SPA) {
SPA spa(graphs, graph_recipe, global, topology, lim);
auto controller = spa.Synthethise();
Expand All @@ -92,6 +98,8 @@ namespace scs::examples {
ExportTopology(topology, dir + "Topology");
if (exec == ExecutionType::AStar) {
GenerateImagesFromDot("../../exports/Hinge/Full/AStar/");
} else if (exec == ExecutionType::GBFS) {
GenerateImagesFromDot("../../exports/Hinge/Full/GBFS/");
} else if (exec == ExecutionType::SPA) {
GenerateImagesFromDot("../../exports/Hinge/Full/SPA/");
}
Expand Down
Loading

0 comments on commit 19cdb70

Please sign in to comment.