// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // This module is in analogy to CondStat0 (which should be read first). It // // behaves different to CondStat0, since it generates the following guarded // // actions: // // * True => error = 0<i&0<i-1 // // * True => assert 1<=i // // Since initially i==0 holds, the expression 0<i&0<i-1 evaluates to false // // since (false&top is false), but the assertion fails. // // See also CondStat0.qrz for comparison. // // ************************************************************************** // module CondExpr0(nat ?i,event !error) { error = (i>0 ? (i-1>0) : false ); } drivenby { nothing; }