Skip to content
Snippets Groups Projects
Commit 90cf5cea authored by Jaime Arias's avatar Jaime Arias
Browse files

revert files

parent faceaf86
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
maude/semantics.maude
+ 32
− 32
View file @ 90cf5cea
......@@ -17,7 +17,7 @@ mod NPTAD-INTERPRETER is
var TS : TickState .
vars L1 L2 L1' L2' : Location .
var ACT : Action .
var AI AI1 AI2 : AutoId .
var AG AG1 AG2 : Agent .
vars RESET RESET1 RESET2 : Resets .
vars G G1 G2 INV INV1 INV2 : Constraint .
vars R1 R2 : RExpr .
......@@ -47,12 +47,12 @@ mod NPTAD-INTERPRETER is
.
crl [local] :
{ NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickNotOk locs: (AI @ L1, LOCS)
{ NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickNotOk locs: (AG @ L1, LOCS)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickOk locs: (AI @ L1', LOCS)
{ NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickOk locs: (AG @ L1', LOCS)
clocks: CVALUES' parameters: PVALUES dvariables: DVVALUES' constraint: CONS' n: N >
if
CVALUES' := reset-clocks(RESET, CVALUES) /\
......@@ -60,20 +60,20 @@ mod NPTAD-INTERPRETER is
--- Guard evaluated with the current values and the invariant at L1' with the new values
CONS' := CONS and
eval(G, CVALUES, PVALUES, DVVALUES) and
inv( ( NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > ),
(AI @ L1') , CVALUES', PVALUES, DVVALUES') /\
inv( ( NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > ),
(AG @ L1') , CVALUES', PVALUES, DVVALUES') /\
smtCheck(CONS')
.
crl [binary] :
{ NET, < AI1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AI2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickNotOk locs: (AI1 @ L1, AI2 @ L2, LOCS)
{ NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickNotOk locs: (AG1 @ L1, AG2 @ L2, LOCS)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET, < AI1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AI2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickOk locs: (AI1 @ L1', AI2 @ L2', LOCS)
{ NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickOk locs: (AG1 @ L1', AG2 @ L2', LOCS)
clocks: CVALUES' parameters: PVALUES dvariables: DVVALUES' constraint: CONS' n: N >
if
CVALUES' := reset-clocks(RESET2, reset-clocks(RESET1, CVALUES)) /\
......@@ -82,9 +82,9 @@ mod NPTAD-INTERPRETER is
CONS' := CONS and
eval(G1, CVALUES, PVALUES, DVVALUES)
and eval(G2, CVALUES, PVALUES, DVVALUES)
and inv( ( NET, < AI1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AI2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > ),
(AI1 @ L1', AI2 @ L2'), CVALUES', PVALUES, DVVALUES') /\
and inv( ( NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > ),
(AG1 @ L1', AG2 @ L2'), CVALUES', PVALUES, DVVALUES') /\
smtCheck(CONS')
.
endm
......@@ -97,7 +97,7 @@ mod NPTAD-INTERPRETER-FME is
var TS : TickState .
vars L1 L2 L1' L2' : Location .
var ACT : Action .
var AI AI1 AI2 : AutoId .
var AG AG1 AG2 : Agent .
vars RESET RESET1 RESET2 : Resets .
vars G G1 G2 INV INV1 INV2 : Constraint .
vars R1 R2 : RExpr .
......@@ -127,12 +127,12 @@ mod NPTAD-INTERPRETER-FME is
.
crl [local] :
{ NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickNotOk locs: (AI @ L1, LOCS)
{ NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickNotOk locs: (AG @ L1, LOCS)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickOk locs: (AI @ L1', LOCS)
{ NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickOk locs: (AG @ L1', LOCS)
clocks: CVALUES' parameters: PVALUES dvariables: DVVALUES' constraint: CONS' n: N >
if
CVALUES' := reset-clocks(RESET, CVALUES) /\
......@@ -142,20 +142,20 @@ mod NPTAD-INTERPRETER-FME is
fme-all( (vars-in-clocks(CVALUES) \ vars-in-clocks(CVALUES')),
CONS and
eval(G, CVALUES, PVALUES, DVVALUES) and
inv( ( NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > ),
(AI @ L1') , CVALUES', PVALUES, DVVALUES')) /\
inv( ( NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > ),
(AG @ L1') , CVALUES', PVALUES, DVVALUES')) /\
smtCheck(CONS')
.
crl [binary] :
{ NET, < AI1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AI2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickNotOk locs: (AI1 @ L1, AI2 @ L2, LOCS)
{ NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickNotOk locs: (AG1 @ L1, AG2 @ L2, LOCS)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET, < AI1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AI2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickOk locs: (AI1 @ L1', AI2 @ L2', LOCS)
{ NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickOk locs: (AG1 @ L1', AG2 @ L2', LOCS)
clocks: CVALUES' parameters: PVALUES dvariables: DVVALUES' constraint: CONS' n: N >
if
CVALUES' := reset-clocks(RESET2, reset-clocks(RESET1, CVALUES)) /\
......@@ -166,9 +166,9 @@ mod NPTAD-INTERPRETER-FME is
CONS
and eval(G1, CVALUES, PVALUES, DVVALUES)
and eval(G2, CVALUES, PVALUES, DVVALUES)
and inv( ( NET, < AI1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AI2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > ),
(AI1 @ L1', AI2 @ L2'), CVALUES', PVALUES, DVVALUES')) /\
and inv( ( NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > ),
(AG1 @ L1', AG2 @ L2'), CVALUES', PVALUES, DVVALUES')) /\
smtCheck(CONS')
.
endm
maude/state.maude
+ 6
− 8
View file @ 90cf5cea
......@@ -14,7 +14,7 @@ load fme .
--- Definition of the state of a PTA: values for discrete variables and clocks
--- as well as the current location for each automaton
--- as well as the current location for each agent/automaton
fmod VALUATION is
pr NETWORK .
pr FOURIER-MOTZKIN .
......@@ -22,8 +22,8 @@ fmod VALUATION is
--- From parameters, clocks, variables and locations to their current values
sorts LocValuation ClockValuation ParValuation DVarValuation .
--- Current location for a given automaton
op _@_ : AutoId Location -> LocValuation [ctor prec 10 format(g g g o)] .
--- Current location for a given automaton/agent
op _@_ : Agent Location -> LocValuation [ctor prec 10 format(g g g o)] .
--- Current value for a clock
op _:_ : Clock RExpr -> ClockValuation [ctor prec 10] .
--- Current value for a parameter
......@@ -153,7 +153,7 @@ fmod STATE is
var N : Nat .
var TS : TickState .
vars L1 L2 L1' L2' : Location .
var AI : AutoId .
var AG AG1 AG2 : Agent .
vars C1 C2 CLOCK : Clock .
vars RESET RESET1 RESET2 : Resets .
vars G G1 G2 INV INV1 INV2 : Constraint .
......@@ -235,8 +235,6 @@ fmod STATE is
eq eval(DVAR != R, CVALUES, PVALUES, DVVALUES) = eval(DVAR, DVVALUES) =/== R .
eq eval(DVAR > R, CVALUES, PVALUES, DVVALUES) = eval(DVAR, DVVALUES) > R .
eq eval(DVAR < R, CVALUES, PVALUES, DVVALUES) = eval(DVAR, DVVALUES) < R .
eq eval(DVAR >= R, CVALUES, PVALUES, DVVALUES) = eval(DVAR, DVVALUES) >= R .
eq eval(DVAR <= R, CVALUES, PVALUES, DVVALUES) = eval(DVAR, DVVALUES) <= R .
--- Discrete Variables
eq eval(DVAR, ((DVAR : R), DVVALUES)) = R .
......@@ -256,7 +254,7 @@ fmod STATE is
--- Extracting the invariants
op inv : Network SetLocValuation SetClockValuation SetParValuation SetDVarValuation -> BoolExpr .
eq inv(NET, empty, CVALUES, PVALUES, DVVALUES) = true .
eq inv( (< AI | (@ L1 inv INV : TRANS ), SSTDEF >, NET),
((AI @ L1) , LOCS) , CVALUES, PVALUES, DVVALUES) =
eq inv( (< AG | (@ L1 inv INV : TRANS ), SSTDEF >, NET),
((AG @ L1) , LOCS) , CVALUES, PVALUES, DVVALUES) =
eval(INV, CVALUES, PVALUES, DVVALUES) and inv(NET, LOCS, CVALUES, PVALUES, DVVALUES) .
endfm
maude/syntax.maude
+ 3
− 5
View file @ 90cf5cea
......@@ -13,7 +13,7 @@ networks of PTAs.
fmod BASE is
sort Location .
sorts Action .
sort AutoId . --- Identifiers for automata
sort Agent . --- Identifiers for automata
sort Clock .
sort Parameter .
sort DVariable . --- Discrete/integer variables
......@@ -61,12 +61,10 @@ fmod CONSTRAINT is
op _>_ : ClockRExpr PTA-LinRExpr -> Constraint [ctor] .
op _>=_ : ClockRExpr PTA-LinRExpr -> Constraint [ctor] .
op _=_ : ClockRExpr PTA-LinRExpr -> Constraint [ctor] .
op _!=_ : DVariable Rat -> Constraint [ctor] .
op _=_ : DVariable Rat -> Constraint [ctor] .
op _!=_ : DVariable Rat -> Constraint [ctor] .
op _<_ : DVariable Rat -> Constraint [ctor] .
op _<=_ : DVariable Rat -> Constraint [ctor] .
op _>_ : DVariable Rat -> Constraint [ctor] .
op _>=_ : DVariable Rat -> Constraint [ctor] .
endfm
--- Reset expressions (including changing values for discrete variables)
......@@ -115,7 +113,7 @@ fmod AUTOMATON is
--- Automaton as a set of locations and transitions
sort Automaton .
op <_|_> : AutoId SetStateDef -> Automaton [ctor] .
op <_|_> : Agent SetStateDef -> Automaton [ctor] .
endfm
view Automaton from TRIV to AUTOMATON is sort Elt to Automaton . endv
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment