 \((\Pri_a(p),e)\) is the action pictured in  Figure 3.  Given an initial pointed Kripke model \((M,w)\) at which p is true, we determine the model-transforming effect of the action \((\Pri_a(p),e)\) by constructing a new pointed Kripke model  \[ (M[\Pri_a(p)],(w,e)). \]   The construction of the Kripke model \(M[\Pri_a(p)]\) is given by the BMS “product update”. 