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

update maude theories

parent 9e73c2b5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
maude/alt-smt.maude
+ 1
− 1
View file @ 08e1c11b
......@@ -202,7 +202,7 @@ endfm
fmod SMT-EXP-TRANS is
protecting REAL-INTEGER-EXPR .
protecting ALT-REAL-INTEGER-EXPR .
protecting META-SMT-CONSTANT-TRANS * (op __ to _#_) . --- to avoid a parsing error
protecting META-SMT-CONSTANT-TRANS * (op __ : NatList NatList -> NatList to _#_) .
op trBool : BoolExpr ~> BooleanExpr .
op trInt : IntExpr ~> IntegerExpr .
......
maude/analysis.maude
+ 1
− 1
View file @ 08e1c11b
......@@ -32,7 +32,7 @@ fmod EXT-META-LEVEL is
op module : Nat Qid -> Module .
eq module(N, Q) =
(mod 'NET-ANALYSIS is
including Q . # extending (if N == 0 then 'NPTAD-INTERPRETER else 'NPTAD-INTERPRETER-FME fi) .
including Q . extending (if N == 0 then 'NPTAD-INTERPRETER else 'NPTAD-INTERPRETER-FME fi) .
sorts none .
none none none none none endm) .
......
maude/semantics.maude
+ 32
− 32
View file @ 08e1c11b
......@@ -17,7 +17,7 @@ mod NPTAD-INTERPRETER is
var TS : TickState .
vars L1 L2 L1' L2' : Location .
var ACT : Action .
var AG AG1 AG2 : Agent .
var AI AI1 AI2 : AutoId .
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, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickNotOk locs: (AG @ L1, LOCS)
{ NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickNotOk locs: (AI @ L1, LOCS)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickOk locs: (AG @ L1', LOCS)
{ NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickOk locs: (AI @ 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, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > ),
(AG @ L1') , CVALUES', PVALUES, DVVALUES') /\
inv( ( NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > ),
(AI @ L1') , CVALUES', PVALUES, DVVALUES') /\
smtCheck(CONS')
.
crl [binary] :
{ 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)
{ 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)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ 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)
{ 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)
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, < 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') /\
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') /\
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 AG AG1 AG2 : Agent .
var AI AI1 AI2 : AutoId .
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, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickNotOk locs: (AG @ L1, LOCS)
{ NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickNotOk locs: (AI @ L1, LOCS)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickOk locs: (AG @ L1', LOCS)
{ NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickOk locs: (AI @ 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, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > ),
(AG @ L1') , CVALUES', PVALUES, DVVALUES')) /\
inv( ( NET, < AI | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > ),
(AI @ L1') , CVALUES', PVALUES, DVVALUES')) /\
smtCheck(CONS')
.
crl [binary] :
{ 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)
{ 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)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ 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)
{ 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)
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, < 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')) /\
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')) /\
smtCheck(CONS')
.
endm
maude/state.maude
+ 8
− 6
View file @ 08e1c11b
......@@ -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 agent/automaton
--- as well as the current location for each 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/agent
op _@_ : Agent Location -> LocValuation [ctor prec 10 format(g g g o)] .
--- Current location for a given automaton
op _@_ : AutoId 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 AG AG1 AG2 : Agent .
var AI : AutoId .
vars C1 C2 CLOCK : Clock .
vars RESET RESET1 RESET2 : Resets .
vars G G1 G2 INV INV1 INV2 : Constraint .
......@@ -235,6 +235,8 @@ 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 .
......@@ -254,7 +256,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( (< AG | (@ L1 inv INV : TRANS ), SSTDEF >, NET),
((AG @ L1) , LOCS) , CVALUES, PVALUES, DVVALUES) =
eq inv( (< AI | (@ L1 inv INV : TRANS ), SSTDEF >, NET),
((AI @ L1) , LOCS) , CVALUES, PVALUES, DVVALUES) =
eval(INV, CVALUES, PVALUES, DVVALUES) and inv(NET, LOCS, CVALUES, PVALUES, DVVALUES) .
endfm
maude/syntax.maude
+ 5
− 3
View file @ 08e1c11b
......@@ -13,7 +13,7 @@ networks of PTAs.
fmod BASE is
sort Location .
sorts Action .
sort Agent . --- Identifiers for automata
sort AutoId . --- Identifiers for automata
sort Clock .
sort Parameter .
sort DVariable . --- Discrete/integer variables
......@@ -61,10 +61,12 @@ 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)
......@@ -113,7 +115,7 @@ fmod AUTOMATON is
--- Automaton as a set of locations and transitions
sort Automaton .
op <_|_> : Agent SetStateDef -> Automaton [ctor] .
op <_|_> : AutoId 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