This article has participated in the activity of “New person creation Ceremony”, and started the road of digging gold creation together.

We have a Beverage Vending Machine, now we need to design a model to count the number of soda and beer, if the Vending Machine is empty, return the inserted coins.

• The difference between data-dependent Systems and TS model is that Location is used to replace the state of TS and Conditional transition is used to replace the transformation relation of TS.

For vending machines:

• Status: start, select
• Conditional transfer:
  1. Start ↪ture: coinselectStart xhookRightarrow []{ture: coin} select startture: coinselect
  2. Start ↪ture: ture: refillStartStart \ xhookRightarrow []{ture: ture:refill} startstartture: ture:refill start

Start indicates that the vending machine is in its initial position

Select indicates that the vending machine is at the position where the coin has been inserted and the beverage is waiting to be selected

Transfer conditions
$g:\alpha$

In vending machines ture:coin and ture:refill, they are transfer conditions, expressed as G :αg:\alphag:α

• GGG represents a Boolean state
• α\alphaα represents an action, and only if GGG is true will the action α\alphaα be executed, otherwise nothing will be executed

We can look at some other conditional transfer processes:

1. When the number of sodas is greater than 0, perform the sget action to get sodas

Start ↪nsoda > 0: sgetStart \xhookrightarrow[]{nsoda > \ 0 \ : sget} start startnsoda > 0: sgetstart 2. Start ↪nbeer > 0: bgetStartStart xhookRightarRow []{nbeer\ > \ 0 \ : \ bget} start startnbeer > 0 : bget start 3. When the number of soda and beer is empty, execute the ret_coin action to return the coin start↪nsoda = 0∧nbeer = 0: ret_coinstartstart \xhookrightarrow[]{nsoda \ = \ 0 \wedge nbeer \ = \ 0 \ : \ ret \_coin} start Startnsoda = 0∧nbeer = 0: ret_coin start

Different effects of different actions:

action	instructions	impact
coin	Put in a coin	There is no
ret_coin	Return the coin	There is no
refill	Refill with soda and beer	nsoda := max; nbeer := max
sget	Get a bottle of soda	nsoda := nsoda -1
bget	Get a bottle of beer	nbeer := nbeer -1

Nsode is the number of sodas, and nbeer is the number of beers

Typed variables

• Concept: A standardized type (such as integer, Boolean, character, etc.) will be associated with variables to model the system

• Var: In the previous examples, nsoda and Nbeer are typed variables, referred to as Var.

• Dom (x) : The value range of each variable x is denoted as the field (DOM). For the digital circuit, the value of the variable can only be 0 or 1, but for the software, the value range of the variable may be very large (such as considering the range of integers in the program), then there is no effective limit with domain, so the concept of domain is introduced. For n variables x=(x1,x2… ,xn)x = (x_{1},x_{2},… ,x_{n})x=(x1,x2,… ,xn), and its field is D=(D1×D2×… ×Dn)D = (D_{1}\times D_{2}\times… \ times D_ D = {n}) (D1 (D2)… (Dn)

• Eval(Var) : The set of all possible results is called Eval(Var), one of which is called the mapping η\etaη. For example, the set of variables x is called η(x)\eta(x)η(x).

• Cond(Var) : The set of all conditions set on a variable, called Cond(Var)

• Effect: Act×Eval(Var)→Eval(Var)Act \times Eval(Var)→Eval(Var)Act ×Eval(Var)→Eval(Var)

• Example: as an action of alpha: : x = y + 5 \ alpha: : x = y + 5 alpha: : x = y + 5 as an example, the variables x and y are evaluated when the initial eta (x) = 17, eta (y) = – 2 eta (x) = 17, \ \ eta (y) = 2 eta (x) = 17, eta (y) = – 2

If do alpha \ alpha alpha to x, then the value of x equals y + 5 finally, namely – 2 + 5 = 3 Effect (alpha, eta) (x) = eta (y) + 5 = – 2 + 5 = 3 Effect (eta), alpha, and eta (y) (x) = \ + 5 = – 2 + 5 = 3 Effect (alpha, η)(x)=η(y)+5=−2+5=3 So the value of y for – 2 Effect (alpha, eta) (y) = eta (y) = – 2 Effect (eta), alpha, and eta (y) (y) = \ = – 2 Effect (alpha, eta) (y) = eta (y) = – 2

Program Graph (PG)

• Concept: A directed graph in which edges connecting different nodes are marked as variables and actions and nodes as positions.
• action
  $action$The effect of “is formalized by mapping, as in the example above with typed variables:
  • 
    $Effect :Act × Eval(Var) \hookrightarrow Eval(Var)$
  • 
    $\alpha \ \ action \ \ x := y+5$
  • 
    $\eta \ evaluation \ \eta(x) = 17, \eta(y) = −2$
  • 
    $Effect(\alpha,\eta)(x)=\eta(y) + 5 =−2 + 5 = 3$
  • 
    $Effect (eta), alpha, and eta (y) (y) = \ = – 2$
• PG is a sextuple
  $PG = (Loc, Act, Effect, \hookrightarrow, Loc_{0}, g_{0})$
  • Loc is a set of locations
  • An Act is a set of actions
  • Effect is Act×Eval(Var)→Eval(Var)Act \times Eval(Var) \ Rightarrow Eval(Var)Act×Eval(Var)→Eval(Var)
  • ↪⊆Loc×Cond(Var)×Act×Loc\hookrightarrow \subseteq Loc\ times Cond(Var) \times Act \times Loc↪⊆Loc×Cond(Var)×Act×Loc, Is a relationship transfer condition
  • Loc0 LocLoc_{0} \subseteq LocLoc0⊆Loc: is a set of initial locations
  • G0 ∈Cond(Var) G_ {0} \in Cond(Var) G0 ∈Cond(Var) : is a set of initial conditions
• In the previous vending machine example
  • 
    $Loc=\{start,select\}$
  • 
    $Loc_{0}=\{start\} \ Var=\{ nsoda,nbeer\}$
  • 
    $Act=\{bget,sget,coin,ret\_coin,refill\}$
  • G0 ={nsoda= Max ∧nbeer= Max}g_{0}=\{nsoda= Max \wedge Nbeer = Max \}g0={nsoda= Max ∧nbeer= Max}g0={nsoda= Max ∧nbeer= Max
  • 
    $Effect:$
    • Effect(coin,η)=ηEffect(coin, eta) = etaEffect(coin,η)=η, indicating that the target variables (nsoda and Nbeer) are not changed when coins are put into the coin
    • Effect(retcoin,η)=ηEffect(ret_coin,\eta) = etaEffect(retcoin,η)=η, indicating that the coin was returned with no change in the target variables (nsoda and Nbeer)
    • Effect(sget,η)=η[nsoda:=nsoda−1]Effect(sget, eta) =nsoda [nsoda:=nsoda−1]Effect(sget, η)= nsoda [nsoda:=nsoda−1] Decrease the value of Nsoda by one
    • Effect(bget,η)=η[nbeer:=nbeer−1]Effect(bget, eta) = eta[nbeer:=nbeer −1]Effect(bget, η)=η[nbeer:=nbeer−1] Nbeer goes down by one
    • Effect (refill, eta) = [nsoda: = Max, nbeer: = Max] Effect (refill, eta) \ = [Nsoda := Max,nbeer:= Max]Effect(η)=[nsoda:= Max,nbeer:= Max], indicating that the values of Nsoda and Nbeer are equal to the maximum value
  • PG figure :(in which, the black solid inside the node represents beer and the hollow represents soda. The initial position in the figure is only two bottles of beer and two bottles of soda)

• Method of converting PG to TS
  • PG sextuples:

PG=(Loc,Act,Effect,↪,Loc0,g0)PG =(Loc,Act,Effect, hookrightarrow, Loc_{0}, G_ {0})PG=(Loc,Act,Effect,↪,Loc0,g0) are position, action, influence, transition relation, initial position, initial qualification respectively -ts sextuple: TS=(S,Act,→,I,AP,L)TS =(S,Act, \rightarrow,I,AP,L)TS =(S,Act, \rightarrow,I,AP,L)TS =(S,Act, \rightarrow,I,AP,L)TS =(S,Act, \rightarrow,I,AP,L)TS =(S,Act, \rightarrow,I,AP,L)TS =(S,Act, \rightarrow,I,AP,L) -s =Loc×Eval(Var)S=Loc \times Eval(Var)S=Loc×Eval(Var), which indicates that the state of TS is the Cartesian product of the position and the value of the variable. In particular, the new state contains the position and the value of the variable at the position – ActActAct remains unchanged – →∈S×Act×S\rightarrow \in S\ times Act \times S→∈S×Act×S is defined by the following rules: ℓ ↪ g: alpha ℓ ‘Sunday afternoon eta ⊨ g ⟨ ℓ, eta ⟩ – alpha ⟨ ℓ’, Effect (alpha, eta) ⟩ \ frac {\ ell \ overset {g: \ alpha} {\ hookrightarrow} {\ ell} ‘eta \ models \ wedge \ g} {\langle \ell , \eta \rangle \overset{\alpha } {\rightarrow} \langle {\ell}’ , Effect (eta) \ alpha, \ \ rangle} ⟨ ℓ, eta ⟩ – alpha ⟨ ℓ ‘, Effect (alpha, eta) ⟩ ℓ ↪ g: alpha ℓ ‘Sunday afternoon eta ⊨ g said, The shift relationship is defined as the current assignment of η\etaη on a state corresponding to their original position ℓ\ellℓ on PG satisfying the executive condition GGG for action α\alphaα, ⟨ L,η \eta \rangle⟨ L,η⟩, ⟨ l ‘to the new state, Effect (alpha, eta) ⟩ \ langle l’, Effect (eta) \ alpha, \ \ rangle ⟨ l ‘, Effect (alpha, eta) ⟩ transfer relationship. Of these, ℓ ‘{\ell}’ℓ’ is their ℓ\ellℓ shift by ↪\hookrightarrow↪ from the ℓ ‘\ellℓ’ position in the original PG, which can be the same for ℓ\ellℓ, And the Effect (alpha, eta) Effect (\ alpha, \eta)Effect(α,η) is the current variable assignment η\etaη by EffectEffectEffect table action α\alphaα corresponding to the new variable assignment (can be the same as η\etaη).

- $I = \ {\ langle \ ell, eta \ rangle \} \ | \ ell \ Loc_ in {0} \ cup \ \ {g in Cond (Var) | eta \ \ models g_ {0} \} $, Represents that the initial state is the Cartesian product of all initial positions in PG and all variables assigned to satisfy the initial condition. - $AP = Loc \cup Cond(Var)$, indicating that the set of atomic propositions is the union of all positions $Loc$and all conditions $Cond(Var)$that occur in PG. - $L = \ {\ ell \} \ cup \ \ {g in Cond (Var) eta \ | \ \ models g} $, said the state take tags get position $\ ell eta $$and variable assignment $\ collection meet the qualification of $g $.Copy the code