Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
ProB Rodin Plugin
Manage
Activity
Members
Labels
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Locked files
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Analyze
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
general
stups
ProB Rodin Plugin
Commits
0e317163
Commit
0e317163
authored
10 years ago
by
Sebastian Krings
Browse files
Options
Downloads
Patches
Plain Diff
a simple port of the ConstructTraceCommand from ProB 2.0
parent
83be5554
No related branches found
No related tags found
No related merge requests found
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
de.prob.core/src/de/prob/core/command/ConstructTraceCommand.java
+194
-0
194 additions, 0 deletions
....core/src/de/prob/core/command/ConstructTraceCommand.java
with
194 additions
and
0 deletions
de.prob.core/src/de/prob/core/command/ConstructTraceCommand.java
0 → 100644
+
194
−
0
View file @
0e317163
/**
* (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
* Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
* (http://www.eclipse.org/org/documents/epl-v10.html)
* */
package
de.prob.core.command
;
import
java.util.ArrayList
;
import
java.util.Collection
;
import
java.util.HashSet
;
import
java.util.LinkedList
;
import
java.util.List
;
import
java.util.Set
;
import
de.be4.classicalb.core.parser.analysis.prolog.ASTProlog
;
import
de.be4.classicalb.core.parser.exceptions.BException
;
import
de.prob.core.Animator
;
import
de.prob.core.domainobjects.Operation
;
import
de.prob.core.domainobjects.State
;
import
de.prob.core.domainobjects.StateError
;
import
de.prob.core.domainobjects.Variable
;
import
de.prob.core.domainobjects.eval.PredicateEvalElement
;
import
de.prob.exceptions.ProBException
;
import
de.prob.parser.ISimplifiedROMap
;
import
de.prob.prolog.output.IPrologTermOutput
;
import
de.prob.prolog.term.CompoundPrologTerm
;
import
de.prob.prolog.term.ListPrologTerm
;
import
de.prob.prolog.term.PrologTerm
;
/**
* Command to execute an event that has not been enumerated by ProB.
*
* @author Jens Bendisposto
*
*/
public
final
class
ConstructTraceCommand
implements
IComposableCommand
{
private
static
final
String
RESULT_VARIABLE_STATES
=
"States"
;
private
static
final
String
RESULT_VARIABLE_OPS
=
"Ops"
;
private
static
final
String
RESULT_VARIABLE_ERRORS
=
"Errors"
;
private
final
List
<
PredicateEvalElement
>
evalElement
;
private
final
List
<
String
>
name
;
private
final
List
<
String
>
errors
=
new
ArrayList
<
String
>();
private
List
<
Integer
>
executionNumber
=
new
ArrayList
<
Integer
>();
public
ConstructTraceCommand
(
final
List
<
String
>
name
,
final
List
<
String
>
predicates
,
Integer
executionNumber
)
{
this
.
name
=
name
;
this
.
evalElement
=
new
ArrayList
<
PredicateEvalElement
>();
for
(
String
string
:
predicates
)
{
try
{
evalElement
.
add
(
PredicateEvalElement
.
create
(
string
));
}
catch
(
BException
e
)
{
throw
new
IllegalArgumentException
(
"Formula must be a predicate: "
+
string
);
}
}
if
(
name
.
size
()
!=
evalElement
.
size
())
{
throw
new
IllegalArgumentException
(
"Must provide the same number of names and predicates."
);
}
int
size
=
this
.
name
.
size
();
for
(
int
i
=
0
;
i
<
size
;
++
i
)
{
this
.
executionNumber
.
add
(
executionNumber
);
}
}
public
ConstructTraceCommand
(
final
List
<
String
>
name
,
final
List
<
String
>
predicate
)
{
this
(
name
,
predicate
,
1
);
}
public
ConstructTraceCommand
(
final
List
<
String
>
name
,
final
List
<
String
>
predicate
,
final
List
<
Integer
>
executionNumber
)
{
this
(
name
,
predicate
);
this
.
executionNumber
=
executionNumber
;
if
(
name
.
size
()
!=
executionNumber
.
size
())
{
throw
new
IllegalArgumentException
(
"Must provide the same number of names and execution numbers."
);
}
}
/**
* This method is called when the command is prepared for sending. The
* method is called by the Animator class, most likely it is not interesting
* for other classes.
*
* @throws ProBException
*
* @see de.prob.animator.command.AbstractCommand#writeCommand(de.prob.prolog.output.IPrologTermOutput)
*/
@Override
public
void
writeCommand
(
final
IPrologTermOutput
pto
)
{
pto
.
openTerm
(
"prob_construct_trace"
);
pto
.
openList
();
for
(
String
n
:
name
)
{
pto
.
printAtom
(
n
);
}
pto
.
closeList
();
final
ASTProlog
prolog
=
new
ASTProlog
(
pto
,
null
);
pto
.
openList
();
for
(
PredicateEvalElement
cb
:
evalElement
)
{
cb
.
getPrologAst
().
apply
(
prolog
);
}
pto
.
closeList
();
pto
.
openList
();
for
(
Integer
n
:
executionNumber
)
{
pto
.
printNumber
(
n
);
}
pto
.
closeList
();
pto
.
printVariable
(
RESULT_VARIABLE_STATES
);
pto
.
printVariable
(
RESULT_VARIABLE_OPS
);
pto
.
printVariable
(
RESULT_VARIABLE_ERRORS
);
pto
.
closeTerm
();
}
public
boolean
hasErrors
()
{
return
!
errors
.
isEmpty
();
}
public
List
<
String
>
getErrors
()
{
return
errors
;
}
@Override
public
void
processResult
(
final
ISimplifiedROMap
<
String
,
PrologTerm
>
bindings
)
throws
CommandException
{
// errors
ListPrologTerm
list
=
(
ListPrologTerm
)
bindings
.
get
(
RESULT_VARIABLE_ERRORS
);
for
(
PrologTerm
prologTerm
:
list
)
{
errors
.
add
(
prologTerm
.
toString
());
}
// Change history in Animator ...
// need to reconstruct operations and states
final
Animator
animator
=
Animator
.
getAnimator
();
ListPrologTerm
operations
=
(
ListPrologTerm
)
bindings
.
get
(
RESULT_VARIABLE_OPS
);
ListPrologTerm
states
=
(
ListPrologTerm
)
bindings
.
get
(
RESULT_VARIABLE_STATES
);
for
(
int
i
=
0
;
i
<
operations
.
size
();
i
++)
{
PrologTerm
operationPrologTerm
=
operations
.
get
(
i
);
Operation
op
=
Operation
.
fromPrologTerm
(
operationPrologTerm
);
// state(NewStateId,StateValues,Initialised,InvKO,MaxOpsReached,Timeout,OpTimeout,StateErrors,UnsatProps,OperationsForState)
CompoundPrologTerm
statePrologTerm
=
(
CompoundPrologTerm
)
states
.
get
(
i
);
ListPrologTerm
stateValuesPrologTerm
=
(
ListPrologTerm
)
statePrologTerm
.
getArgument
(
2
);
List
<
Variable
>
stateValues
=
new
LinkedList
<
Variable
>();
for
(
PrologTerm
prologTerm
:
stateValuesPrologTerm
)
{
stateValues
.
add
(
new
Variable
((
CompoundPrologTerm
)
prologTerm
));
}
ListPrologTerm
stateErrorsPrologTerm
=
(
ListPrologTerm
)
statePrologTerm
.
getArgument
(
8
);
Collection
<
StateError
>
stateErrors
=
new
LinkedList
<
StateError
>();
for
(
PrologTerm
prologTerm
:
stateErrorsPrologTerm
)
{
stateErrors
.
add
(
new
StateError
((
CompoundPrologTerm
)
prologTerm
));
}
Set
<
String
>
opTimeouts
=
new
HashSet
<
String
>(
PrologTerm
.
atomicStrings
((
ListPrologTerm
)
statePrologTerm
.
getArgument
(
7
)));
ArrayList
<
Operation
>
enabledOperations
=
new
ArrayList
<
Operation
>();
for
(
PrologTerm
enop
:
(
ListPrologTerm
)
statePrologTerm
.
getArgument
(
10
))
{
final
CompoundPrologTerm
cpt
=
(
CompoundPrologTerm
)
enop
;
enabledOperations
.
add
(
Operation
.
fromPrologTerm
(
cpt
));
}
State
s
=
new
State
(
statePrologTerm
.
getArgument
(
1
).
toString
(),
statePrologTerm
.
getArgument
(
2
).
toString
().
equals
(
"true"
),
statePrologTerm
.
getArgument
(
3
).
toString
().
equals
(
"true"
),
statePrologTerm
.
getArgument
(
5
).
toString
().
equals
(
"true"
),
statePrologTerm
.
getArgument
(
4
).
toString
().
equals
(
"true"
),
stateValues
,
enabledOperations
,
stateErrors
,
opTimeouts
);
animator
.
getHistory
().
add
(
s
,
op
);
animator
.
announceCurrentStateChanged
(
s
,
op
);
}
}
}
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment