diff --git a/examples/src/main/scala/soda/tiles/fairness/example/childcaresubsidy/CcsPerChildPipeline.soda b/examples/src/main/scala/soda/tiles/fairness/example/childcaresubsidy/CcsPerChildPipeline.soda new file mode 100644 index 0000000..60ff8e8 --- /dev/null +++ b/examples/src/main/scala/soda/tiles/fairness/example/childcaresubsidy/CcsPerChildPipeline.soda @@ -0,0 +1,77 @@ + +directive lean +import Soda.tiles.fairness.tool.TileMessage +import Soda.tiles.fairness.tile.AtLeastTile +import Soda.tiles.fairness.tile.NeededPTile +import Soda.tiles.fairness.tile.ReceivedSigmaPTile +import Soda.tiles.fairness.tile.UnzipPairFstTile +import Soda.tiles.fairness.tile.UnzipPairSndTile +import Soda.tiles.fairness.tile.ZipTile + + +/** + * This pipeline returns 'true' when all the actors in the input receive a resource that + * satisfies their needs, and 'false' otherwise. + */ + +class CcsPerChildPipeline + + abstract + sigma : Measure -> Measure -> Measure + children : Actor -> Measure + utility : Resource -> Measure + + all_equal_tile = AllEqualTile .mk + + received_sigma_p_tile = ReceivedSigmaPTile .mk (sigma) (utility) + + children_tile = AttributePTile .mk (children) + + all_actor_pair_tile = AllActorPairTile .mk + + _division_with_2 (val0 : Int) (val1 : Int) : Measure = + if val1 == 0 + then None + else Some (val0 / val1) + + _division_with (val0 : Int) (m1 : Measure) : Measure = + match m1 + case Some (val1) ==> _division_with_2 (val0) (val1) + case None ==> None + + division (m0 : Measure) (m1 : Measure) : Measure = + match m0 + case Some (val0) ==> _division_with (val0) (m1) + case None ==> None + + division_tile = SigmaTile .mk (division) + + unzip_fst_tile = UnzipPairFstTile .mk + + unzip_snd_tile = UnzipPairSndTile .mk + + zip_tile = ZipTile .mk + + get_branch_0 (message : TileMessage [Seq [TilePair [Actor] [Actor] ] ] ) + : TileMessage [Seq [Measure] ] = + received_sigma_p_tile .apply (unzip_fst_tile .apply (message) ) + + get_branch_1 (message : TileMessage [Seq [TilePair [Actor] [Actor] ] ] ) + : TileMessage [Seq [Measure] ] = + children_tile .apply (unzip_snd_tile .apply (message) ) + + zip_branches (message : TileMessage [Seq [TilePair [Actor] [Actor] ] ] ) + : TileMessage [Seq [TilePair [Measure] [Measure] ] ] = + zip_tile .apply (get_branch_0 (message) ) (get_branch_1 (message) ) + + apply (message : TileMessage [Boolean] ) : TileMessage [Boolean] = + all_equal_tile .apply ( + division_tile .apply ( + zip_branches ( + all_actor_pair_tile .apply (message) + ) + ) + ) + +end + diff --git a/examples/src/main/scala/soda/tiles/fairness/example/childcaresubsidy/Package.scala b/examples/src/main/scala/soda/tiles/fairness/example/childcaresubsidy/Package.scala index 90dccc6..1d7d38d 100644 --- a/examples/src/main/scala/soda/tiles/fairness/example/childcaresubsidy/Package.scala +++ b/examples/src/main/scala/soda/tiles/fairness/example/childcaresubsidy/Package.scala @@ -79,6 +79,93 @@ object CcsNoSubsidyPipeline { } +/* +directive lean +import Soda.tiles.fairness.tool.TileMessage +import Soda.tiles.fairness.tile.AtLeastTile +import Soda.tiles.fairness.tile.NeededPTile +import Soda.tiles.fairness.tile.ReceivedSigmaPTile +import Soda.tiles.fairness.tile.UnzipPairFstTile +import Soda.tiles.fairness.tile.UnzipPairSndTile +import Soda.tiles.fairness.tile.ZipTile +*/ + +/** + * This pipeline returns 'true' when all the actors in the input receive a resource that + * satisfies their needs, and 'false' otherwise. + */ + +trait CcsPerChildPipeline +{ + + def sigma : Measure => Measure => Measure + def children : Actor => Measure + def utility : Resource => Measure + + lazy val all_equal_tile = AllEqualTile .mk + + lazy val received_sigma_p_tile = ReceivedSigmaPTile .mk (sigma) (utility) + + lazy val children_tile = AttributePTile .mk (children) + + lazy val all_actor_pair_tile = AllActorPairTile .mk + + private def _division_with_2 (val0 : Int) (val1 : Int) : Measure = + if ( val1 == 0 + ) None + else Some (val0 / val1) + + private def _division_with (val0 : Int) (m1 : Measure) : Measure = + m1 match { + case Some (val1) => _division_with_2 (val0) (val1) + case None => None + } + + def division (m0 : Measure) (m1 : Measure) : Measure = + m0 match { + case Some (val0) => _division_with (val0) (m1) + case None => None + } + + lazy val division_tile = SigmaTile .mk (division) + + lazy val unzip_fst_tile = UnzipPairFstTile .mk + + lazy val unzip_snd_tile = UnzipPairSndTile .mk + + lazy val zip_tile = ZipTile .mk + + def get_branch_0 (message : TileMessage [Seq [TilePair [Actor, Actor] ] ] ) + : TileMessage [Seq [Measure] ] = + received_sigma_p_tile .apply (unzip_fst_tile .apply (message) ) + + def get_branch_1 (message : TileMessage [Seq [TilePair [Actor, Actor] ] ] ) + : TileMessage [Seq [Measure] ] = + children_tile .apply (unzip_snd_tile .apply (message) ) + + def zip_branches (message : TileMessage [Seq [TilePair [Actor, Actor] ] ] ) + : TileMessage [Seq [TilePair [Measure, Measure] ] ] = + zip_tile .apply (get_branch_0 (message) ) (get_branch_1 (message) ) + + def apply (message : TileMessage [Boolean] ) : TileMessage [Boolean] = + all_equal_tile .apply ( + division_tile .apply ( + zip_branches ( + all_actor_pair_tile .apply (message) + ) + ) + ) + +} + +case class CcsPerChildPipeline_ (sigma : Measure => Measure => Measure, children : Actor => Measure, utility : Resource => Measure) extends CcsPerChildPipeline + +object CcsPerChildPipeline { + def mk (sigma : Measure => Measure => Measure) (children : Actor => Measure) (utility : Resource => Measure) : CcsPerChildPipeline = + CcsPerChildPipeline_ (sigma, children, utility) +} + + trait CcsPerFamilyPipeline { diff --git a/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/CcsPerChildPipelineSpec.soda b/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/CcsPerChildPipelineSpec.soda new file mode 100644 index 0000000..82eca5f --- /dev/null +++ b/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/CcsPerChildPipelineSpec.soda @@ -0,0 +1,28 @@ + +class CcsPerChildPipelineSpec () + extends + AnyFunSuite + + check [A : Type] (obtained : A) (expected : A) : org.scalatest.compatible.Assertion = + assert (obtained == expected) + + _mm = ChildCareSubsidyScenarioExample .mk + + all_cases = _mm .all_cases + + per_child_pipeline = + CcsPerChildPipeline .mk (_mm .measure_sum) (_mm .actor_children) (_mm .resource_value) + + test ("per child on all outcomes") ( + check ( + obtained := all_cases + .map (lambda scenario --> + per_child_pipeline .apply (scenario) .contents + ) + ) ( + expected := Seq (true , false , false , false , true , false , false , true) + ) + ) + +end + diff --git a/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/CcsPerFamilyPipelineSpec.soda b/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/CcsPerFamilyPipelineSpec.soda index ac0d667..d035943 100644 --- a/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/CcsPerFamilyPipelineSpec.soda +++ b/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/CcsPerFamilyPipelineSpec.soda @@ -10,14 +10,14 @@ class CcsPerFamilyPipelineSpec () all_cases = _mm .all_cases - no_subsidy_pipeline = + per_family_pipeline = CcsPerFamilyPipeline .mk (_mm .measure_sum) (_mm .resource_value) test ("per family on all outcomes") ( check ( obtained := all_cases .map (lambda scenario --> - no_subsidy_pipeline .apply (scenario) .contents + per_family_pipeline .apply (scenario) .contents ) ) ( expected := Seq (true , true , true , false , false , false , false , false) diff --git a/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/CcsSingleGuardianPipelineSpec.soda b/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/CcsSingleGuardianPipelineSpec.soda index 1bdfd84..adb10dc 100644 --- a/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/CcsSingleGuardianPipelineSpec.soda +++ b/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/CcsSingleGuardianPipelineSpec.soda @@ -10,14 +10,14 @@ class CcsSingleGuardianPipelineSpec () all_cases = _mm .all_cases - no_subsidy_pipeline = + single_guardian_pipeline = CcsSingleGuardianPipeline .mk (_mm .measure_sum) (_mm .resource_value) (_mm .actor_adults) test ("single guardian on all outcomes") ( check ( obtained := all_cases .map (lambda scenario --> - no_subsidy_pipeline .apply (scenario) .contents + single_guardian_pipeline .apply (scenario) .contents ) ) ( expected := Seq (true , false , false , true , false , false , false , false) diff --git a/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/Package.scala b/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/Package.scala index 2a3dcdc..9419f10 100644 --- a/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/Package.scala +++ b/examples/src/test/scala/soda/tiles/fairness/example/childcaresubsidy/Package.scala @@ -76,6 +76,35 @@ case class CcsNoSubsidyPipelineSpec () } +case class CcsPerChildPipelineSpec () + extends + AnyFunSuite +{ + + def check [A ] (obtained : A) (expected : A) : org.scalatest.compatible.Assertion = + assert (obtained == expected) + + private lazy val _mm = ChildCareSubsidyScenarioExample .mk + + lazy val all_cases = _mm .all_cases + + lazy val per_child_pipeline = + CcsPerChildPipeline .mk (_mm .measure_sum) (_mm .actor_children) (_mm .resource_value) + + test ("per child on all outcomes") ( + check ( + obtained = all_cases + .map ( scenario => + per_child_pipeline .apply (scenario) .contents + ) + ) ( + expected = Seq (true , false , false , false , true , false , false , true) + ) + ) + +} + + case class CcsPerFamilyPipelineSpec () extends AnyFunSuite @@ -88,14 +117,14 @@ case class CcsPerFamilyPipelineSpec () lazy val all_cases = _mm .all_cases - lazy val no_subsidy_pipeline = + lazy val per_family_pipeline = CcsPerFamilyPipeline .mk (_mm .measure_sum) (_mm .resource_value) test ("per family on all outcomes") ( check ( obtained = all_cases .map ( scenario => - no_subsidy_pipeline .apply (scenario) .contents + per_family_pipeline .apply (scenario) .contents ) ) ( expected = Seq (true , true , true , false , false , false , false , false) @@ -117,14 +146,14 @@ case class CcsSingleGuardianPipelineSpec () lazy val all_cases = _mm .all_cases - lazy val no_subsidy_pipeline = + lazy val single_guardian_pipeline = CcsSingleGuardianPipeline .mk (_mm .measure_sum) (_mm .resource_value) (_mm .actor_adults) test ("single guardian on all outcomes") ( check ( obtained = all_cases .map ( scenario => - no_subsidy_pipeline .apply (scenario) .contents + single_guardian_pipeline .apply (scenario) .contents ) ) ( expected = Seq (true , false , false , true , false , false , false , false)