Imitator
Download
Input
Models
From benchmarks
fig1-DCLXZL18
brp
CSMACD
CSMACDbc10
CSMACDbc5
CSMACDbc6
CSMACDbc9
AndOr
IMPO
IMPOloop
coffee
coffeeDrinker-toolpaper
coffeeDrinker
coffeeDrinkerUnbounded
LALSD14-AIP
LALSD14-FMS1
LALSD14-FMS1p
LALSD14-FMS2p
LALSD14-fig16
LALSD14-fig16p
JLR-TACAS13
JLR15fig5
counterexACSD15
ex-Zeno-basic
ex-Zeno-basic2
ex-Zeno-basic3
ex-Zeno-basic4
ex-Zeno-basic5
ex1pPTA
ex2CM-DLime
exActTimingSynth
exMultiAlgo1
exPQ-inefficient
exSynthPMin-infimum
exSynthTMin-infimum
exU-noloop-infinity
exU-noloop
gt-exPQ-inefficient
gt-exSynthPMin-infimum
gt-exSynthTMin-infimum
F10
F2
F3-nonparam
F3
F4
F5
FischerAHV93
fischer-obs
fischerHRSV02-2
fischerHRSV02-3
fischerHRSV02_obs
fischerPAT2
fischerPAT3
fischerPAT_obs
fischer_2
flipflop
flipflop4D
AndGate
NorGate
NotGate
OrGate
ii3AndGate
iiAndGate
maler_2_4
maler_3_4
maler_3_4_inst
maler_4_4
latchValmem
NoodlesCooking
NuclearPlant
pacemaker-DKKM14
pacemaker-JPMAM12
WAH19-fig1
WHS17-fig1
accel_1000
accel_10000
accel_2000
accel_3000
accel_4000
accel_5000
accel_6000
accel_7000
accel_8000
accel_9000
blowup-1000
blowup-200
blowup-400
blowup-600
blowup-800
gear_1000
gear_10000
gear_2000
gear_3000
gear_4000
gear_5000
gear_6000
gear_7000
gear_8000
gear_9000
packaging
Pipeline-KP12-2-3
Pipeline-KP12-2-5
Pipeline-KP12-3-2
Pipeline-KP12-3-3
RCP-CS01
RCP
RCP3D
simop2
simop3
spsmall
SRlatch
SRlatch_fixed_delay
LA02_2
LA02_2_2.5
LA02_3
am02
astrium_basic_thermal_fp
bb
concurent_tasks_chain
full_cpr08
generic_edf
generic_fp
hppr10_audio
preemptive_maler
Web-privacy-problem
TemperatureController
therac25
ANPS17-fig2a
BlT09-fig1
Train1PTA
TrainAHV93
train-intruder-converted-parameters
train-intruder
train-intruder2
train-intruder3
train-intruder4
Cycle1
synthN
synthRplus
WFAS-BBLS15-det
WFAS-BBLS15
nowick
Property
From benchmarks
brp-pi0
brp-v0
brp
CSMACD-BC
CSMACD-IM
CSMACD
AndOr-pattern
AndOr-pi0
AndOr-v0
IMPO-IM
IMPO
IMPOloop-IM
IMPOloop-IMnontermination
IMPOloop
coffee-BC
coffee-IM
coffee
coffeeDrinker-IM
coffeeDrinker-toolpaper-IM
coffeeDrinker-toolpaper-prop1
coffeeDrinker-toolpaper-prop2
coffeeDrinker-toolpaper-prop3
coffeeDrinker
coffeeDrinkerUnbounded
LALSD14-AIP-BClearn
LALSD14-AIP
LALSD14-FMS1
LALSD14-FMS1p-BClearn
LALSD14-FMS2
LALSD14-fig16
LALSD14-fig16p
JLR-TACAS13-PRPC
JLR-TACAS13
counterexACSD15
ex-Zeno-basic
ex1pPTA
ex2CM-DLime
exActTimingSynth
exMultiAlgo1
exPQ-inefficient
exSynthPMin-infimum
exSynthTMin-infimum
gt-exPQ-inefficient
gt-exSynthPMin-infimum
gt-exSynthTMin-infimum
Fi-BC
Fi-IM
Fi
FischerAHV93
fischer-obs
fischerHRSV02-2
fischerHRSV02-3
fischerHRSV02-BC
fischerHRSV02-IM
fischerHRSV02_obs
fischerPAT-BC
fischerPAT-IM
fischerPAT2
fischerPAT3
fischerPAT_obs
fischer_2-IM
fischer_2
flipflop-IMbad
flipflop
maler_2_4
maler_3_4
maler_4_4
latchValmem-BC
latchValmem-IM
NoodlesCooking
NuclearPlant
pacemaker-JPMAM12
WAH19-fig1
WHS17-fig1
accel
blowup
gear
packaging-PRP
packaging-PRPC
packaging
Pipeline-KP12-2-3
Pipeline-KP12-2-5
Pipeline-KP12-3-2
Pipeline-KP12-3-3
RCP-CS01
RCP
simop
spsmall
SRlatch
am02
therac25
Train1PTA
TrainAHV93
train-intruder
Cycle1
synthN
synthRplus
WFAS-BBLS15-IMgood
WFAS-BBLS15-IMtimeout
WFAS-BBLS15
nowick
Options
Imitator Version
latest
develop
v3.4.0-alpha2
v3.4.0-alpha
3.2.0
3.1.0
3.1.0-beta
3.0.0
3.0.0-beta
2.12.1
Run
Results
Models:
Property:
Options:
Outputs:
Generated files:
Stop