Skip to content

Commit

Permalink
Merge pull request #8 from julianmendez/development
Browse files Browse the repository at this point in the history
Example for child care subsidy
  • Loading branch information
julianmendez authored Mar 7, 2024
2 parents 9627ee5 + 5f25d28 commit eac3694
Show file tree
Hide file tree
Showing 6 changed files with 229 additions and 8 deletions.
Original file line number Diff line number Diff line change
@@ -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

Original file line number Diff line number Diff line change
Expand Up @@ -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
{

Expand Down
Original file line number Diff line number Diff line change
@@ -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

Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -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)
Expand Down

0 comments on commit eac3694

Please sign in to comment.