  Within the printing industry, much of the variety in printed applications
comes from the variety in finishing. Finishing comprises the processing of
sheets of paper after being printed, e.g. to form books. The configuration
space of finishers, i.e. all possible configurations given the available
features and hardware capabilities, are large. Current control software
minimally assists operators in finding useful configurations. Using a classical
modelling and integration approach to support a variety of configuration spaces
is suboptimal with respect to operatability, development time, and maintenance
burden.
  In this paper, we explore the use of a modeling language for finishers to
realize optimizing decision making over configuration parameters in a
systematic way and to reduce development time by generating control software
from models.
  We present CSX, a domain-specific language for high-level declarative
specification of finishers that supports specification of the configuration
parameters and the automated exploration of the configuration space of
finishers. The language serves as an interface to constraint solving, i.e., we
use low-level SMT constraint solving to find configurations for high-level
specifications. We present a denotational semantics that expresses a
translation of CSX specifications to SMT constraints. We describe the
implementation of the CSX compiler and the CSX programming environment (IDE),
which supports well-formedness checking, inhabitance checking, and interactive
configuration space exploration. We evaluate CSX by modelling two realistic
finishers. Benchmarks show that CSX has practical performance (<1s) for several
scenarios of configuration space exploration.
