Modeling Choice in Co-Design

Abstract

This report describes a method for modeling free and forced choice within Co-Design. In a free choice among a set, one has control over which option is selected, while in a forced choice one does not. Given a preorder P describing resources or functionalities, a free choice among a subset of P acts like a meet. Dually, a forced choice acts like a join. Moreover, the two types of choice distribute over one another. Based on this, we construct a universal model for choice on a preorder using the free completely distributive lattice ULP. Feasibility relations are then extended to these models. Along the way, we illustrate how to work within ULP and provide results that simplify calculations. The definitions presented here have been implemented in Haskell.