Whilst a simulation provides the intuition behind the ripple-carry adder, using the PRISM model checker we can query the output of all three adders after 10 s to confirm if the correct output is present. We have four input species per adder, excluding the carry, which represent two numbers. We expect one species from each adder as output, representing the addition of two inputs, plus the carry. The third adder relies on the previous adder’s carry being correct. We therefore only need to look at the desired output of each adder plus the carry of the final adder. We summarise this with the following example PRISM property:\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\begin{aligned}&P =? [ \text { true } U <= 10 ( (A_{abridgeOneOut}> Th) \text { and }\\&(B_{bbridgeZeroOut}> Th) \text { and } ( C_{cbridgeOneOut}> Th) \text { and }\\&(C_{cbridgeCarryOneOut} > Th) ) ] \end{aligned}$$\end{document}P=?[trueU<=10((AabridgeOneOut>Th)and(BbbridgeZeroOut>Th)and(CcbridgeOneOut>Th)and(CcbridgeCarryOneOut>Th))]With this example we can only satisfy these three outputs and the carry, by seeing each of their molecular concentrations rise above the threshold Th, based on a specific input configuration. This particular input are the species representing 0 and 1 for the first adder (for example \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$A_{aOneZeroIn}$$\end{document}AaOneZeroIn and \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$A_{aTwoOneIn}$$\end{document}AaTwoOneIn), the species representing inputs 1,1 for the second adder and 1,1 for the third adder. \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$0 + 1$$\end{document}0+1 in the first adder should give us an outcome of 1 carry 0 and so satisfies \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$A_{abridgeOneOut} > Th$$\end{document}AabridgeOneOut>Th. \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$1 + 1$$\end{document}1+1 plus the 0 carry from the first adder gives an output of 0 carry 1, and so satisfies \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$B_{bbridgeZeroOut} > Th$$\end{document}BbbridgeZeroOut>Th. An input of 1 + 1 plus 1 carry from the second adder means that our output should be 1 as well as the final carry should be 1, represented by \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$C_{cbridgeOneOut} > Th$$\end{document}CcbridgeOneOut>Th and \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$C_{cbridgeCarryOneOut} > Th$$\end{document}CcbridgeCarryOneOut>Th. Our adder satisfies this property based upon the inputs given and therefore shows correct operation for an adder.